Research

References with citations can be found on Google Scholar

Below are abstracts of some recent papers by me and my co-authors, as well as links to copies of the papers. The papers are organized by research topic.

Semantics of Quantum Programming Languages

The following papers are from a Multi University Research Initiative whose goal is to lay foundations for semantics and tools for high-level functional quantum programming languages. The Tulane team, consisting of me and my postdocs, has focused on adding recursion to such languages. More information about the project, including the member institutions and the research emanating from the project can be found at this link

LNL-FPC: The Linear / Non-linear Fixpoint Calculus, B. Lindenhovius, M Mislove and V. Zamdzhiev, Logical Methods in Computer Science, to appear. In this paper, we describe a type system with mixed linear and non-linear recursive types called LNL-FPC (the linear/non-linear fixpoint calculus). The type system supports linear typing which enhances the safety properties of programs, but also supports non-linear typing as well which makes the type system more convenient for programming. Just as in FPC, we show that LNL-FPC supports type-level recursion which in turn induces term- level recursion. We also provide sound and computationally adequate categorical models for LNL-FPC which describe the categorical structure of the substructural operations of Intuitionistic Linear Logic at all non-linear types, including the recursive ones. In order to do so, we describe a new technique for solving recursive domain equations within cartesian categories by constructing the solutions over pre-embeddings. The type system also enjoys implicit weakening and contraction rules which we are able to model by identifying the canonical comonoid structure of all non-linear types. We also show that the requirements of our abstract model are reasonable by constructing a large class of concrete models that have found applications not only in classical functional programming, but also in emerging programming paradigms that incorporate linear types, such as quantum programming and circuit description programming languages. This is an extended journal version of the following paper.

Mixed linear and non-linear recursive types, B. Lindenhovius, M. Mislove and V. Zamdzhiev, Proc. ACM Program. Lang., 3(ICFP):111:1–111:29, August 2019. In this paper, we describe a type system with mixed linear and non-linear recursive types called LNL-FPC (the linear/non-linear fixpoint calculus). The type system supports linear typing which enhances the safety properties of programs, but also supports non-linear typing as well which makes the type system more convenient for programming. Just like in FPC, we show that LNL-FPC supports type-level recursion which in turn induces term-level recursion. We also provide sound and computationally adequate categorical models for LNL-FPC which describe the categorical structure of the substructural operations of Intuitionistic Linear Logic at all non-linear types, including the recursive ones. In order to do so, we describe a new technique for solving recursive domain equations within the category CPO by constructing the solutions over pre-embeddings. The type system also enjoys implicit weakening and contraction rules which we are able to model by identifying the canonical comonoid structure of all non-linear types. We also show that the requirements of our abstract model are reasonable by constructing a large class of concrete models that have found applications not only in classical functional programming, but also in emerging programming paradigms that incorporate linear types, such as quantum programming and circuit description programming languages.

Enriching a linear/non-linear lambda calculus: A programming language for string diagrams, B. Lindenhovius, M. Mislove and V. Zamdzhiev, In: Anuj Dawar and Erich Grädel, editors, Proceedings of the 33rd Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2018, Oxford, UK, July 09-12, 2018, pages 659–668. ACM, 2018. Linear/non-linear (LNL) models, as described by Benton, soundly model a LNL term calculus and LNL logic closely related to intuitionistic linear logic. Every such model induces a canonical enrichment that we show soundly models a LNL lambda calculus for string diagrams, introduced by Rios and Selinger (with primary application in quantum computing). Our abstract treatment of this language leads to simpler concrete models compared to those presented so far. We also extend the language with general recursion and prove soundness. Finally, we present an adequacy result for the diagram-free fragment of the language which corresponds to a modified version of Benton and Wadler’s adjoint calculus with recursion.

Semantics for a Lambda Calculus for String Diagrams, B. Lindenhovius. M. Mislove and V. Zamdzhiev. This is an expanded, journal version of the previous listing. In: Outstanding Contributions to Logic (Volume for Samson Abramsky), Lecture Notes in Computer Science, Springer-Verlag, to appear. Preprint.

Probabilistic Models

Completing simple valuations in K-categories, X. Jia and M. Mislove, arxiv.org/abs/2002.01865, Submitted. We prove that Keimel and Lawson’s K-completion Kc of the simple valuation monad Vs defines a monad Kc o Vs on each K-category A. We also characterize the Eilenberg-Moore algebras of Kc o Vs as the weakly locally convex K-cones, and its algebra morphisms as the continuous linear maps. In addition, we explicitly describe the distributive law of Vs over Kc, which allows us to show that the K-completion of any locally convex (respectively, weakly locally convex, locally linear) topological cone is a locally convex (respectively, weakly locally convex, locally linear) K-cone. We also give an example – the Cantor tree with a top – that shows the dcpo-completion of the simple valuations is not the D-completion of the simple valuations in general, where D is the category of monotone convergence spaces and continuous maps.

Domains and stochastic processes. Theoretical Computer Science 807 (2020) (also Domains and random variables). The aim of this paper is to establish a theory of random variables on domains. Our main result shows how to capture a core result from stochastic process theory — Skorohod’s Theorem – using a domain-theoretic approach. The key idea is to use the Cantor tree to prove that each Borel subprobability measure on a Polish space is the push forward of Lebesgue measure by a measurable map by defining an approximating sequence of simple measures each of which can be similarly realized using Scott-continuous maps. The construction also allows a proof that the measurable mappings each realizing measure in a weakly convergent sequence of subprobability measures on a Polish space converge a.s. wrt Lebesgue measure to a measurable map that realizes the limit measure on the Polish space. 

Anatomy of a domain of continuous random variables I. Theoretical Computer Science 546 (2014). This is the first of two papers that examine a construction of a domain of continuous random variables with values in bounded complete domains. The results were first obtained by Goubault-Larrecq and Varacca and presented in their LICS 2011 paper. In this paper, we investigate the structure of the thin probability measures on the bounded complete domain of finite and infinite words over a finite alphabet. 

Anatomy of a domain of continuous random variables II. pdf version. In: Computation, Logic, Games, and Quantum Foundations. The Many Facets of Samson Abramsky, Lecture Notes in Computer Science Volume 7860, 2013, pp 225-245. This is the second of two papers that examine a construction of a domain of continuous random variables with values in bounded complete domains first devised by Goubault-Larrecq and Varacca and presented in their LICS 2011 paper. In this paper, we apply the results from our first paper on this subject to present a detailed construction of the domain of continuous random variables based on the domain of finite and infinite words over a finite alphabet, and taking values in a bounded complete domain. Our construction generalizes the construction of Goubault-Larrecq and Varacca, who restricted attention to the case of a two-letter alphabet. Our investigation confirms that the monad laws are valid, but it reveals that the Kleisli extension needed to define the monad on BCD, the category of bounded complete domains, is not Scott continuous. We leave as an open problem whether the construction can be rescued to obtain a monad on BCD.

Discrete Random Variables over Domains, pdf file. (Theoretical Computer Science 380(2007), pp. 181-198). This is the journal version of the next listing. In this paper we initiate the study of discrete random variables over domains. Our work is inspired by work of Daniele Varacca, who devised indexed valuations as models of probabilistic computation within domain theory. The approach relies on new results about commutative monoids defined on domains that also allow actions of the non-negative reals. Using this approach, we define two such families of real domain monoids, one of which allows us to recapture Varacca’s construction of the Plotkin indexed valuations over a domain. Each of these families leads to the construction of a family of discrete random variables over domains, the second of which forms the object level of a continuous endofunctor on the categories RB (domains that are retracts of bifinite domains), and on FS (domains where the identity map is the directed supremum of deflations finitely separated from the identity). The significance of this last result lies in the fact that there is no known category of continuous domains that is closed under the probabilistic power domain, which forms the standard approach to modeling probabilistic choice over domains. The fact that RB and FS are Cartesian closed and also are closed under a power domain of discrete random variables means we can now model, e.g., the untyped lambda calculus extended with a probabilistic choice operator, implemented via random variables.

Discrete random variables over domains. pdf version. (Proceedings ICALP 2005, LNCS 3580(2005), pp. 1006-1017.) In this paper we explore discrete random variables over domains. We show that these lead to a continuous endofunctor on the categories RB (domains that are retracts of bifinite domains), and FS (domains where the identity map is the directed supremum of deflations finitely separated from the identity). The significance of this result lies in the fact that there is no known category of continuous domains that is closed under the probabilistic power domain, which forms the standard approach to modeling probabilistic choice over domains. The fact that RB and FS are cartesian closed and also are closed under the discrete random variables power domain means we can now model, e.g., the untyped lambda calculus extended with a probabilistic choice operator, implemented via random variables.

Concurrency Theory

Axioms for probability and nondeterminism, (with Joel Ouaknine and James Worrell). pdf version. (Appeared in the Proceedings of EXPRESS 2003, ENTCS.) This paper presents a domain model for a process algebra featuring both probabilistic and nondeterministic choice. The former is modelled using the probabilistic powerdomain of Jones and Plotkin, while the latter is modelled by a geometrically convex variant of the Plotkin powerdomain. The main result is to show that the expected laws for probability and nondeterminism are sound and complete with respect to the model. We also present an operational semantics for the process algebra, and we show that the domain model is fully abstract with respect to probabilistic bisimilarity.

Nondeterminism and probabilistic choice: obeying the laws, preprint. pdf version.(Appeared in CONCUR 2000.) In this paper we describe how to build semantic models that support both nondeterministic choice and probabilistic choice. Several models exist that support both of these constructs, but none that we know of satisfies all the laws one would like. Using domain-theoretic techniques, we show how models can be devised using the “standard model” for probabilistic choice, and then applying modified domain-theoretic models for nondeterministic choice. These models are distinguished by the fact that the expected laws for nondeterministic choice and probabilistic choice remain valid. We also describe some potential applications of our model to aspects of security. 

A truly concurrent semantics for a process algebra using resource pomsets, preprint. PostScripttm version. PDF version. (joint with Paul Gastin, LAIFA, Université Paris VII) (Appeared in Theoretical Computer Science.) In this paper we extend the language in “A truly concurrent semantics for a simple parallel programming language” to include a hiding operator a lá CSP. In our language concurrency is taken as a primitive operator, rather than being defined in terms of parallel composition and nondeterminism. In fact, our language does not support nondeterministic choice. Our treatment of hiding is novel, in that we record the unwinding of recursion, so that divergence is observable. This avoids our having to assume that divergence is catastrophic, as is done in CSP. Still it is possible to regain a more traditional semantics by simply hiding the resources that unwinding recursions use. We present both an SOS-style operational semantics for our language, as well as a denotational model based on resource pomsets, a generalization of the notion of resource trace that was used in the earlier paper. In addition, we show our denotational model is adequate and fully abstract with respect to the behavior function which extracts from the operational semantics only the set of strings of actions a process can execute. 

A truly concurrent semantics for a simple parallel programming language, preprint (joint work with Paul Gastin), Extended abstract, Full paper in pdf format, Full paper in PostScripttm version. (Appeared in CSL 1999; journal version in Mathematical Structures for Computer Science.) This paper (for which the first link is an extended abstract) presents a simple programming language which uses the concatenation operator of trace theory as its basic operator (as opposed to sequential composition, which is more traditional in process algebra). Heretofore, denotational models supporting this operator have proved elusive because the concatenation operator is not monotone. This barrier has been overcome by the work of Diekert and Gastin and the work of Gastin and Teodesiu, which has provided domain-theroetic models for concatenation. In this paper, we utilize the resource traces model of Gastin and Teodesiu as the basis for our denotational model. This allows us to include in our language a restriction operator which restricts processes to a prescribed subset of the resources, and we also include synchronization on channels (represented again as subsets of the resource set), as well as process variables and recursion. We give an operational semantics for our language in the traditional SOS style, and we show that the behavior of processes as defined by this semantics is the same as the denotational mapping our denotational semantics defines on the language – i.e., our operational semantics is congruent to our denotational semantics. 

Trace theory and state explosion, preprint, pdf version. This short paper, which appeared in the Proceedings of PDPTA’99, explores the relationship between partial order methods in model checking and the simple programming language described in the previous paper. In the model-checking community, partial order methods are used to reduce the number of paths of computation that need to be checked. This is accomplished by defining an independence relation on transitions in the system under study, and then performing a selective search that produces a representative path to be checked for each set of independent computations. The main result in this paper shows that such independence relations can be realized as the relation on the simple language studied in the previous paper induced by the denotational mapping. This allows one to code up the words of the language accepted by the automaton of the concurrent system that is being model-checked as processes in the language of that paperso that words of the automaton are independent if and only if they are represented by independent processes in the language. 

Denotational Models for Unbounded Nondeterminism This paper is an extended abstract which appeared in the Proceedings of MFPS 11, which took place at Tulane in 1995. The Proceedings is Volume 1 of ENTCS, and the paper can be found there. The paper presents a domain-theoretic approach to devising models for unbounded nondeterminism. Using local cpos as the basis for modeling unbounded nondeterminism, the results show that there is no analogue for the lower power domain to support unbounded nondeterminism, but that there is a cartesian closed category which includes an analogue to the upper power domain for unbounded nondeterminism, and in which the mappings all have least fixed points. Left open is the question whether there is an analogue for the convex power domain for unbounded nondeterminism; while the claim is made in the paper that no such object exists, the example presented only shows that the “obvious candidate” will not suffice, because it is not a local cpo.

Fixed Points Without Completeness, Programming Research Group Technical Report 93-1, 54pp., Theoretical Computer Science 138 (1995), 273 – 314 (with S. A. Schneider and A. W. Roscoe) This paper develops the theory of local cpo’s, which are ordered spaces which are not necessarily complete, and establishes a dominated convergence theorem which which guarantees that functions with pre-fixed points have fixed points. This theory then is applied to give a denotational semantics for a dialect of Timed CSP which supports unbounded nondeterminism. For a copy of the paper, send email to me at mwm AT math.tulane.edu. 

Full Abstraction and Recursion, Theoretical Computer Science 151 (1995), 207 – 256 (with F. J. Oles). This paper shows how an operational model and related adequate and fully abstract denotational model for a base language can be extended to models for the language of closed terms for the language extended to include identifiers and recursion operators. The paper also presents new notions which are called order adequacy and order full abstraction which arise naturally because of the assumptions that the operational and denotational models both are ordered spaces. For a copy of the paper, send email to me at mwm AT math.tulane.edu. 

Full Abstraction and Unnested Recursion, Lecture Notes in Computer Science 666(1993),pp. 384-397 (with F. J. Oles). This paper starts with a “base language” without identifiers and an operational model and related denotational model which is adequate and fully abstract for the operational model. Then it is shown how to extend the operational and denotational models to ones for an extension of the language which supports recursion through systems of recursive equations so that the extended denotational model again is adequate and fully abstract with respect to the extended operational model. 

Domain Theory

From Haar to Lebesgue via Domain Theory In: van Breugel F., Kashefi E., Palamidessi C., Rutten J. (eds) Horizons of the Mind. A Tribute to Prakash Panangaden. Lecture Notes in Computer Science  8464 (2014), DOI: doi.org/10.1007/978-3-319-06880-0_11. In this paper, we show that any two group structures on the Cantor set have the same Haar measure, and we also should that each Haar measure maps to Lebesgue measure on the unit interval under the canonical mapping from the Cantor set to the unit interval. 

Monoids over domains (Mathematical Structures in Computer Science 16 (2006), pp. 255-277.) preprint in pdf format. In this paper, we describe three distinct monoids over domains, each with a commutative analog, the latter of which define bagdomain monoids. Our results were inspired by work by Varacca. and they lead to a constructive approach to his \emph{Hoare indexed valuations}. We use our constructive approach to show that the laws Varacca lists as characterizing the Hoare indexed valuations are not complete for the construction he gives. Our construction reveals the missing law, and we also indicate how to repair his construction so that the laws he lists do characterize the construction.

Measuring the probabilistic power domain, (with Keye Martin and James Worrell.) Extended abstract from ICALP 2002; journal version from TCS.) In this paper we show that under modest conditions, a measurement on a domain D lifts in a natural way to a measurement on the probabilistic power domain V(D). 

Local DCPOs, local cpos and local completions, pdf version. This is an extended abstract of the paper I presented at MFPS 15, which took place at Tulane in April, 1999. A revised version appeared in the Proceedings of the conference, which is Volume 20 of ENTCS. The paper shows how local cpos (those in which only the lower set of a point is a cpo) can be used to provide bounded complete models for topological spaces. A construction using the bounded Scott-closed sets is given that provides such a model for any topological space that has a domain-theroetic model. This last means that the space is homeomorphic to the maximal elements of a continuous dcpo which itself is weak at the top (i.e., the relative Scott and Lawson topologies agree on the maximal elements of the dcpo). For example, the model for Polish spaces devised by Lawson and the formal ball model of Edalat and Heckmann both satisfy this criterion, and so these models can be “converted to” bounded complete (local cpo) models. 

Generalizing domain theory, preprint, pdf version. (Appeared in the Proceedings of FOSSACS 1998.) This is a revised version of an extended abstract that is drawn from my address at the first ETAPS conference in Lisbon in March, 1998. The paper reviews some of the basic aspects of domain theory, and then goes on to describe a number of generalizations that have arisen in response to solving problems with domain-theoretic techniques, but for which domain theory per se did not apply. 

Topology, domain theory and theoretical computer science, preprint,pdf version. (Appeared in Topology and Its Applications.) This is a survey paper that resulted from the lectures on Topology and Theoretical Computer Science which I gave at the 1996 Summer Topology Conference in Portland, Maine. The paper reviews some of the central results about domain theory and its applications to theoretical computer science with an eye toward demonstrating why order theory together with topology — i.e., domain theory — have played such a prominent role in applications to theoretical computer science. There are some new results in the paper, including a new derivation of the classical power domains and some results about models of the lambda-I calculus. The latter were pointed out to the author by Furio Honsell (Udine) after the lecture on models of the untyped lambda calculus that was one of the lectures in the series.

Corrigendum, pdf copy. Jean Goubault-Larrecq pointed out an error in the proof of Proposition 4.45 of this paper. In this short note, we correct that proof, and also give a simpler proof that the convex power domain of a coherent domain is again coherent.

A Characterization of Linear FS-Lattices, preprint, (with Michael Huth) pdf version. A continuous lattice is a linear FS-lattice if the identity map is the directed supremum of selfmaps that are finitely separated from the identity. These lattices recently have been used to provide semantic models for linear logic. In this note, we show that a continuous lattice is linear FS if and only if its function space of sup-preserving selfmaps is a Scott-continuous projection of its function space of Scott-continuous selfmaps. Further, we show that a continuous lattice is completely distributive if and only if the function space of sup-preserving self maps is a sup-projection of its function space of Scott-continuous self maps. We also investigate the structure of the space of selfmaps of certain prototypical continuous lattices that fail to be linear FS lattices. 

Using duality to solve domain equations. This is an extended abstract that appeared in the Proceedings of MFPS 12, which took place at CMU in 1997. The Proceedings is Volume 6 of ENTCS, and the paper can be found there. The paper examines the role of the duality between the categories of cpos and upper adjoints and cpos and lower adjoints in solving domain equations. It is shown that a number of domain equations can be shown to have a solution simply by applying this duality. It also is shown that the duality theory allows the equations in question to be solved in the simpler setting of partially ordered sets and monotone mappings. Moreover, it is shown that the results also hold in the more general setting of abstract bases and ideal maps, a category introduced in this paper.

Adjunctions Between Categories of Domains, Fundamenta Informaticae, 22 (1995), 93 – 116 (with F. J. Oles) pdf version. This paper explores adjunctions between various categories of domains and lluf subcategories of the category of Scott domains and Scott continuous functions; ie, those subcategories whose objects are all Scott domains, but whose morphisms are more limited. After recasting the Hoare power domain in this setting, two adjunctions using the Smyth power domain are considered. The first is the traditional Smyth power domain functor, while the second uses the same construct on objects, but varies the morphisms. Finally, a new adjunction is explored which associates to domain its family of Scott-closed subsets. The paper also explores this construction as an information system. 

All Compact Hausdorff Lambda Model are Degenerate, Fundamenta Informaticae,22(1995), 23 – 52 (with K. H. Hofmann) pdf version This paper shows that there are no non-degenerate compact Hausdorff models for the untyped lambda calculus, thus limiting the possible models within the category of Hausdorff k-spaces. This is of interest since Hausdorff k-spaces forms a cartesian closed category, so eliminating this category would give further credence to the idea that cpo’s are intrinsic to models of the typed lambda calculus. The paper also includes a recasting of Meyer’s seminal results on lambda models within topological categories, as opposed to the category of sets.

Testing and Labelled Markov Processes

Testing semantics: Connecting processes and process logics, (with Dusko Pavlovic and James Worrell), (to appear in Proceedings of AMAST 2006, LNCS.) pdf version We propose a methodology based on testing as a framework to capture the interactions of a machine represented in a denotational model and the data it manipulates. Using a connection that models machines on the one hand, and the data they manipulate on the other, testing is used to capture the interactions of each with the objects on the other side: just as the data that are input into a machine can be viewed as tests that the machine can be sub jected to, the machine can be viewed as a test that can be used to distinguish data. While this approach is based on duality theories that now are common in semantics, it accomplishes much more than simply moving from one side of the duality to the other; it faithfully represents the interactions that embody what is happening as the computation proceeds. Our basic philosophy is that tests can be used as a basis for modeling interactions, as well as processes and the data on which they operate. In more abstract terms, tests can be viewed as formulas of process logics, and testing semantics connects processes and process logics, and assigns computational meanings to both. 

Duality for labelled Markov processes, (with Joel Ouaknine, Dusko Pavlovic and James Worrell). pdf version. Labelled Markov processes (LMPs) are probabilistic automata with a measurable state space. In this paper we present a `universal’ LMP as the Stone-Gelfand-Naimark dual of a C*-algebra consisting of formal linear combinations of labelled trees. We characterize the state space of the universal LMP as the set of homomorphims from an ordered commutative monoid of labelled trees into the multiplicative unit interval. This yields a simple semantics for LMPs which is fully abstract with respect to probabilistic bisimilarity. We also consider LMPs with entry points and exit points in the framework of Elgot’s iterative theories. We define an iterative theory of LMPs by specifying its categorical dual: a category of commutative rings consisting of C*-algebras of trees and `shapely maps’ between them. We find that the basic operations for composing, refining, programming LMPs have simple definitions in the dual category.

Domains, testing and simulation for labelled Markov processes, (with Franck van Breugel, Joel Ouaknine and James Worrell). pdf version. (Extended abstract in FOSSACS 2003(next listing); journal version appeared in TCS.) This paper gives a fundamental characterization of approximate bisimilarity in terms of the notion of (exact) probabilistic similarity. In particular, we show that the topology of approximate bisimilarity is the Lawson topology with respect to the simulation preorder. To complement this abstract characterization we give a statistical account of probabilistic similarity, and by extension, of approximate bisimilarity, in terms of the process testing formalism of Larsen and Skou.

An intrinsic characterization of approximate probabilistic bisimilarity, (with F. van Breugel, J. Ouaknine and J. Worrell). (Appeared in the Proceedings of FOSSACS 2003, LNCS.) pdf version; journal version is previous listing.) In previous work we have investigated a notion of approximate bisimilarity for labelled Markov processes. We argued that such a notion is more realistic and more feasible to compute than (exact) bisimilarity. The main technical tool used in the underlying theory was the Hutchinson metric on probability measures. This paper gives a more fundamental characterization of approximate bisimilarity in terms of the notion of (exact) similarity. In particular, we show that the topology of approximate bisimilarity is the Lawson topology with respect to the simulation preorder. To complement this abstract characterization we give a statistical account of similarity, and by extension, of approximate bisimilarity, in terms of the process testing formalism of Larsen and Skou.

Security

Aaron Jaggard (DIMACS), Catherine Meadows (NRL), Roberto Segala (Verona) and I worked on the task-based PIOA model of concurrency used by Canetti, Lynch, Segala and others to model security and crypto-protocols. PIOAs, probabilistic input/output automata, are a model for concurrent computation first devised by Nancy Lynch (MIT) and Roberto Segala (Verona). The notion of a task was introduced into the work with Canetti as a means for restricting the power of the adversary, making the model more realistic for applications to security. The main result obtained by Canetti, et al has been a model for oblivious transfer that includes reasoning about cryptographic primitives, rather than the more traditional “Dolev-Yao” approach that assumes perfect cryptography. For a more precise description of this work and a list of publication see Ling Cheung’s Task-PIOA and Security Verification web page. 

Our work devised an approach to PIOAs using domain theory to establish results about discrete probability, which lie at the heart of the PIOA model. Our results show how to model the Dining Cryptographers using the task-based PIOA approach.

Notes from DIMACS pdf version. This is a working draft outlining our approach to modeling task-based PIOAs using domain theory. The main theoretical result is a proof that the semantic task scheduler that corresponds to a syntactic task schedule is deterministic, rather than being randomized, as is done in the Canetti, Lynch, Segala et al work

Reasoning About Probabilistic Security Using Task-PIOAs pdf version.(ARSPA-WITS, Lecture Notes in Computer Science 6186 (2010), Springer, pp. 2-22.) This paper presents our approach to task-based PIOAs using order theory (since all processes are finite, there is no need for the full power of domain theory). The paper also presents a functional simulation result that is useful when analyzing situations in which the only difference between the processes being compared is the secret each one has. We illustrate the approach by analyzing the Dining Cryptographers protocol. The approach is notable for the fact that treatment includes reasoning about the actions of a Master who chooses who pays, first analyzing the situation of a deterministic Master, and then devising a proof for a Master that chooses the payer probabilistically by leveraging the proof in the deterministic case.