Michael W. Mislove
Pendergraft Herbert Buchanan Professor
Department of Mathematics
Tulane University

Address: Department of Mathematics
         Tulane University 
         New Orleans, LA 70118

Email:   
    	 
Office:  Gibson 400C
Phone:  +1 504 862-3441
FAX:    +1 504 865-5063

• Mathematics: Topological Algebra, Domain Theory, Ordered Structures, Category Theory, Non-well-founded Set Theory
• Theoretical Computer Science: Semantics of High-level Programming Languages, Concurrency Theory, Process Algebra and Probabilistic Models

Editorial Information

Here is information about the journals for which I am an editor:

• Semigroup Forum - Editor.
  The Forum is a journal devoted to the theory of semigroups and to its applications. It is publisher by Springer Verlag (New York, Heidelberg, Berlin). Submissions to this journal can be made to me or any of the other editors of the journal; more information may be obtained by using this link. If you wish to submit an article to me, you should send me an electronic version of the submission, preferably as a pdf file. While there is no required format for submissions, accepted papers must be submitted as TeX or LaTeX files.
• Mathematical Structures in Computer Sceince - Member, Editorial Board.
  Mathematical Structures in Computer Science focuses on the application of mathematics and mathematical logic to computer science. To submit a paper, obtain the instructions for authors at this page.

• Theoretical Computer Science - Editor.
  TCS is devoted to research in the theoretical aspects of computer science. It is published by Elsevier Science Publishers (Holland). If you wish o submit a paper to TCS, you should go to the TCS web site, where you will find instructions about how to submit papers for publication in the journal. During the online submission process, you will be asked to name an editor who you wish to handle your submission. You can name one, or else the Editor-in-Chief for the relevant part of TCS will assign one for you.
• Electronic Notes in Theoretical Computer Science - Managing Editor.
  Electronic Notes in Theoretical Computer Science was founded in order to allow the use of the World Wide Web to disseminate the proceedings of conferences, lecture notes and topical monographs more efficiently and rapidly than the print media allow. ENTCS is published using the facilities of Elsevier Science B. V., and under its auspices. Access the URL http://www.entcs.org to find information about submitting proposals for volumes for publication in the series. Anyone whose home institution maintains a subscription to and of Elsevier's theory journals, Information and Computation, JCSS, IPL or Theoretical Computer Science has free access to the ENTCS archive at Elsevier.
  If you are preparing a paper for an ENTCS volume, you should go to the ENTCS Macro Home Page for precise instructions about how to prepare your submission.

Slides from Some Recent Talks

• Here are the slides from my talk, "Random Bits of Noise" given at the 25th Conference on the Mathematical Foundations of Programming Semantics, at Oxford, 2009.

• Here are the slides from my talk, "Probabilistic Automata, Probabilistic Models and Crypto-protocols" given at the Protocol eXchange Meeting, Naval Postgraduate School, January, 2009.

• Here are the slides from my talk at the Workshop on Formal and Computational Cryptography which was a satellite workshop of LICS + CSF Conferences at CMU in June, 2008.

• Here are the slides from my investiture as the Pendergraft Herbert Buchanan Professor of Mathematics, May 5, 2008. Note: These are best viewed in a separate pdf file viewer such as Abobe Reader rather than within a browser.

  Here are some pictures from the investiture ceremony.

• Here are the slides from my talk on Variations on an Integral Domain Theme which was an invited address at the Conference Honoring Peter Collins and Mike Reed held at Oxford in August, 2006.

• Here are the slides from my talk on Testing Semantics: Processes vs Logics at the AMAST 2006 meeting. This is based on the paper below with Dusko Pavlovic and James Worrell.

• Here are the slides from my talk at ICALP 2005 on discrete random variables over domains.
• Here are the slides from my talk on "Probability and Domain Theory" at the Workshop on Domains VII held August 29 - September 1, 2004 at the Technische Universität Darmstadt, Germany.
• Here is a pdf file containing slides from a talk given at the Monterey Workshop, 2001, and at the Modélisation et Vérification Seminar, LIAFA, Université Paris VII in June, 2001. There also is a copy of the slides in PostScript. The talk concerned some ideas about modeling probabilistic choice in CSP and presents some ideas about a potential application to hybrid systems.

Research Papers

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

• 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. PostScript^tm 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 nondetermistic 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 PostScript^tm 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 langauge 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 paper so 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.

• Discrete Random Variables over Domains, pdf file. (To appear, Special Issue of Theoretical Computer Science devoted to selected papers from ICALP 2005). This is the journal version of the next listing.
Abstract: In this paper we initiate the study of discrete random variables over domains. Our work is inspired by work of Deniele 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. (Appeared in the Proceedings of ICALP 2005, LNCS.) 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.
• 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-theroetic 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.
• 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 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.

• Notes from Dimacs This is a working draft outlining our approah 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. pdf version.

• Reasoning About Probabilistic Security Using Task-PIOAs This paper presents our approach to task-based PIOAs using order theory (since all processes are finite, there is no need for teh 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 Cryptograhers 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. The paper is under submission to this year's ARSPA-WITS satellite workshop at ETAPS 2010. pdf version.