Probabilistic π-Calculus and Event Structures

This paper proposes two semantics of a probabilistic variant of the π-calculus: an interleaving semantics in terms of Segala automata and a true concurrent semantics, in terms of probabilistic event structures. The key technical point is a use of types to identify a good class of non-deterministic probabilistic behaviours which can preserve a compositionality of the parallel operator in the event structures and the calculus. We show an operational correspondence between the two semantics. This allows us to prove a “probabilistic confluence” result, which generalises the confluence of the linearly typed π-calculus.     

A View on Decoherence Via Master Equations

This paper addresses the discussion on probabilistic features of the concept of decoherence as it appeared in quantum physics. Given a Lindblad-type generator of an open system dynamics, we derive applicable criteria to characterize decoherent behaviour.Presented at the International Conference “Entanglement, Information & Noise”, Krzyżowa, Poland, June 14-20, 2004.Partially supported by FONDECYT grant 1030552.     

A Calculus of Terms for Coalgebras of Polynomial Functors

A syntax and semantics of types, terms and formulas for coalgebras of polynomial functors is developed, extending earlier work [4] on monomial coalgebras to include functors constructed using coproducts. A modified ultrapower construction for polynomial coalgebras is introduced, adapting the conventional ultrapower to retain only those states that evaluate observable terms in a standard way.A special role is played by terms that take observable values and are “rigid”: their free variables do not occur in any state-valued subterm. The following “co-Birkhoff” theorem is proved: a class of polynomial coalgebras is definable by Boolean combinations of equations between rigid terms iff the class is closed under disjoint unions, images of bisimulations, and observable ultrapowers.     

A Proof Search Specification of the π-Calculus

We present a meta-logic that contains a new quantifier (for encoding “generic judgments”) and inference rules for reasoning within fixed points of a given specification. We then specify the operational semantics and bisimulation relations for the finite π-calculus within this meta-logic. Since we restrict to the finite case, the ability of the meta-logic to reason within fixed points becomes a powerful and complete tool since simple proof search can compute this one fixed point. The quantifier helps with the delicate issues surrounding the scope of variables within π-calculus expressions and their executions (proofs). We shall illustrate several merits of the logical specifications we write: they are natural and declarative; they contain no side conditions concerning names of variables while maintaining a completely formal treatment of such variables; differences between late and open bisimulation relations are easy to see declaratively; and proof search involving the application of inference rules, unification, and backtracking can provide complete proof systems for both one-step transitions and for bisimulation.     

Completeness of Continuation Models for λμ-Calculus

We show that a certain simple call-by-name continuation semantics of Parigot's λ_μ-calculus is complete. More precisely, for every λ_μ-theory we construct a cartesian closed category such that the ensuing continuation-style interpretation of λ_μ, which maps terms to functions sending abstract continuations to responses, is full and faithful. Thus, any λ_μ-category in the sense of L. Ong (1996, in “Proceedings of LICS '96,” IEEE Press, New York) is isomorphic to a continuation model (Y. Lafont, B. Reus, and T. Streicher, “Continuous Semantics or Expressing Implication by Negation,” Technical Report 93-21, University of Munich) derived from a cartesian-closed category of continuations. We also extend this result to a later call-by-value version of λ_μ developed by C.-H. L. Ong and C. A. Stewart (1997, in “Proceedings of ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, Paris, January 1997,” Assoc. Comput. Mach. Press, New York).     

Non-Decomposable Quantum Dynamical Semigroups and Bound Entangled States

We use open quantum system techniques to construct one-parameter semigroups of positive maps and apply them to study the entanglement properties of a class of 16-dimensional density matrices, representing states of a 4 × 4 bipartite system.Presented at the International Conference “Entanglement, Information & Noise”, Krzyżowa, Poland, June 14–20, 2004.     

A Novel Stochastic Game Via the Quantitative μ-calculus

The quantitative μ-calculus qMμ extends the applicability of Kozen's standard μ-calculus [D. Kozen, Results on the propositional μ-calculus, Theoretical Computer Science 27 (1983) 333–354] to probabilistic systems. Subsequent to its introduction [C. Morgan, and A. McIver, A probabilistic temporal calculus based on expectations, in: L. Groves and S. Reeves, editors, Proc. Formal Methods Pacific '97 (1997), available at [PSG, Probabilistic Systems Group: Collected reports, http://web.comlab.ox.ac.uk/oucl/research/areas/probs/bibliography.html]; also appears at [A. McIver, and C. Morgan, “Abstraction, Refinement and Proof for Probabilistic Systems,” Technical Monographs in Computer Science, Springer, New York, 2005, Chap. 9], M. Huth, and M. Kwiatkowska, Quantitative analysis and model checking, in: Proceedings of 12th annual IEEE Symposium on Logic in Computer Science, 1997] it has been developed by us [A. McIver, and C. Morgan, Games, probability and the quantitative μ-calculus qMu, in: Proc. LPAR, LNAI 2514 (2002), pp. 292–310, revised and expanded at [A. McIver, and C. Morgan, Results on the quantitative μ-calculus qMμ (2005), to appear in ACM TOCL]; also appears at [A. McIver, and C. Morgan, “Abstraction, Refinement and Proof for Probabilistic Systems,” Technical Monographs in Computer Science, Springer, New York, 2005, Chap. 11], A. McIver, and C. Morgan, “Abstraction, Refinement and Proof for Probabilistic Systems,” Technical Monographs in Computer Science, Springer, New York, 2005, A. McIver, and C. Morgan, Results on the quantitative μ-calculus qMμ (2005), to appear in ACM TOCL] and by others [L. de Alfaro, and R. Majumdar, Quantitative solution of omega-regular games, Journal of Computer and System Sciences 68 (2004) 374–397]. Beyond its natural application to define probabilistic temporal logic [C. Morgan, and A. McIver, An expectation-based model for probabilistic temporal logic, Logic Journal of the IGPL 7 (1999), pp. 779–804, also appears at [A. McIver, and C. Morgan, “Abstraction, Refinement and Proof for Probabilistic Systems,” Technical Monographs in Computer Science, Springer, New York, 2005, Chap.10]], there are a number of other areas that benefit from its use.One application is stochastic two-player games, and the contribution of this paper is to depart from the usual notion of “absolute winning conditions” and to introduce a novel game in which players can “draw”.The extension is motivated by examples based on economic games: we propose an extension to qMμ so that they can be specified; we show that the extension can be expressed via a reduction to the original logic; and, via that reduction, we prove that the players can play optimally in the extended game using memoryless strategies.     

Probabilistic logic programming

Of all scientific investigations into reasoning with uncertainty and chance, probability theory is perhaps the best understood paradigm. Nevertheless, all studies conducted thus far into the semantics of quantitative logic programming have restricted themselves to non-probabilistic semantic characterizations. In this paper, we take a few steps towards rectifying this situation. We define a logic programming language that is syntactically similar to the annotated logics of Blair et al., 1987 and Blair and Subrahmanian, 1988, 45–73) but in which the truth values are interpreted probabilistically. A probabilistic model theory and fixpoint theory is developed for such programs. This probabilistic model theory satisfies the requirements proposed by Fenstad (in “Studies in Inductive Logic and Probabilities” (R. C. Jeffrey, Ed.), Vol. 2, pp. 251–262, Univ. of California Press, Berkeley, 1980) for a function to be called probabilistic. The logical treatment of probabilities is complicated by two facts: first, that the connectives cannot be interpreted truth-functionally when truth values are regarded as probabilities; second, that negation-free definite-clause-like sentences can be inconsistent when interpreted probabilistically. We address these issues here and propose a formalism for probabilistic reasoning in logic programming. To our knowledge, this is the first probabilistic characterization of logic programming semantics.     

Reductions among number theoretic problems

Many number theoretic problems such as integer factorization and the discrete logarithm problem have defied all attempts to classify their complexities. Thirteen such problems are considered, none of which is known either to have a deterministic polynomial time solution, or to be complete for any natural complexity class. Failing this, the next best goal is to determine which among these are the “easiest” and which are the “hardest” problems. Toward this end, this paper gives an overview of reductions among the problems. Two reductions are new: a deterministic polynomial time reduction from squarefreeness to Euler's function φ(n), and a probabilistic polynomial time reduction from order modulo a prime power to discrete logarithm modulo a prime power.     

Lifting Infinite Normal Form Definitions From Term Rewriting to Term Graph Rewriting

nfinite normal forms are a way of giving semantics to non-terminating rewrite systems. The notion is a generalization of the Böhm tree in the lambda calculus. It was first introduced in [Ariola, Z. M. and S. Blom, Cyclic lambda calculi, in: Abadi and Ito [Abadi, M. and T. Ito, editors, “Theoretical Aspects of Computer Software,” Lecture Notes in Computer Science 1281, Springer Verlag, 1997], pp. 77–106] to provide semantics for a lambda calculus on terms with letrec. In that paper infinite normal forms were defined directly on the graph rewrite system. In [Blom, S., “Term Graph Rewriting - syntax and semantics,” Ph.D. thesis, Vrije Universiteit Amsterdam (2001)] the framework was improved by defining the infinite normal form of a term graph using the infinite normal form on terms. This approach of lifting the definition makes the non-confluence problems introduced into term graph rewriting by substitution rules much easier to deal with. In this paper, we give a simplified presentation of the latter approach.     

A Temporal Logic for Proving Properties of Topologically General Executions

We present a generalization of the temporal propositional logic of linear time which is useful for stating and proving properties of the generic execution sequence of a parallel program or a non-deterministic program. The formal system we present is exactly that same as the third of three logics presented by Lehmann and Shelah (Information and Control53, 165–198 (1982)), but we give it a different semantics. The models are tree models of arbitrary size similar to those used in branching time temporal logic. The formulation we use allows us to state properties of the “co-meagre” family of paths, where the term “co-meagre” refers to a set whose complement is of the first category in Baire's classification looking at the set of paths in the model as a metric space. Our system is decidable, sound, and, complete for models of arbitrary size, but it has the finite model property; namely, every sentence having a model has a finite model.     

A Coalgebraic Semantics for Epistemic Programs

This paper gives a fresh look at my previous work on “epistemic actions” and information updates in distributed systems, from a coalgebraic perspective. I show that the “relational” semantics of epistemic programs, given in [BMS2] in terms of epistemic updates, can be understood in terms of functors on the category of coalgebras and natural transformations associated to them. Then, I introduce a new, alternative, more refined semantics for epistemic programs: programs as “epistemic coalgebras”. I argue for the advantages of this second semantics, from a semantic, heuristic, syntactical and proof-theoretic point of view. Finally, as a step towards a generalization, I show these concepts make sense for other functors, and that apparently unrelated concepts, such as Bayesian belief updates and process transformations, can be seen to arise in the same way as our “epistemic actions”.     

A logic for reasoning about probabilities

We consider a language for reasoning about probability which allows us to make statements such as “the probability of E₁ is less than ” and “the probability of E₁ is at least twice the probability of E₂,” where E₁ and E₂ are arbitrary events. We consider the case where all events are measurable (i.e., represent measurable sets) and the more general case, which is also of interest in practice, where they may not be measurable. The measurable case is essentially a formalization of (the propositional fragment of) Nilsson's probabilistic logic. As we show elsewhere, the general (nonmeasurable) case corresponds precisely to replacing probability measures by Dempster-Shafer belief functions. In both cases, we provide a complete axiomatization and show that the problem of deciding satisfiability is NP-complete, no worse than that of propositional logic. As a tool for proving our complete axiomatizations, we give a complete axiomatization for reasoning about Boolean combinations of linear inequalities, which is of independent interest. This proof and others make crucial use of results from the theory of linear programming. We then extend the language to allow reasoning about conditional probability and show that the resulting logic is decidable and completely axiomatizable, by making use of the theory of real closed fields.     

A framework for specifying and verifying the behaviour of open systems

Coding no longer represents the main issue in developing software applications. It is the design and verification of complex software systems that require to be addressed at the architectural level, following methodologies which permit us to clearly identify and design the components of a system, to understand precisely their interactions, and to formally verify the properties of the systems. Moreover, this process is made even more complicated by the advent of the “network-centric” model of computation, where open systems dynamically interact with each other in a highly volatile environment. Many of the techniques traditionally used for closed systems are inadequate in this context.We illustrate how the problem of modeling and verifying behavioural properties of open system is addressed by different research fields and how their results may contribute to a common solution. Building on this, we propose a methodology for modeling and verifying behavioural aspects of open systems. We introduce the IP-calculus, derived from the π-calculas process algebra so as to describe behavioural features of open systems. We define a notion of partial correctness, acceptability, in order to deal with the intrinsic indeterminacy of open systems, and we provide an algorithmic procedure for its effective verification.     

Structured coalgebras and minimal HD-automata for the -calculus

The coalgebraic framework developed for the classical process algebras, and in particular its advantages concerning minimal realizations, does not fully apply to the π-calculus, due to the constraints on the freshly generated names that appear in the bisimulation.In this paper we propose to model the transition system of the π-calculus as a coalgebra on a category of name permutation algebras and to define its abstract semantics as the final coalgebra of such a category. We show that permutations are sufficient to represent in an explicit way fresh name generation, thus allowing for the definition of minimal realizations.We also link the coalgebraic semantics with a slightly improved version of history dependent (HD) automata, a model developed for verification purposes, where states have local names and transitions are decorated with names and name relations. HD-automata associated with agents with a bounded number of threads in their derivatives are finite and can be actually minimized. We show that the bisimulation relation in the coalgebraic context corresponds to the minimal HD-automaton.     

Process expressions and Hoare's logic: Showing an irreconcilability of context-free recursion with Scott's induction rule

In this paper processes specifiable over a non-uniform language are considered. The language contains constants for a set of atomic actions and constructs for alternative and sequential composition. Furthermore it provides a mechanism for specifying processes recursively (including nested recursion). We consider processes as having a state: atomic actions are to be specified in terms of observable behaviour (relative to initial states) and state transformations. Any process having some initial state can be associated with a transition system representing all possible courses of execution. This leads to an operational semantics in the style of Plotkin. The partial correctness assertion {α} p{β} expresses that for any transition system associated with the process p and having some initial state satisfying α, its final states representing successful execution satisfy β. A logic in the style of Hoare, containing a proof system for deriving partial correctness assertions, is presented. This proof system is sound and relatively complete, so any partial correctness assertion can be evaluated by investigating its derivability. Included is a short discussion about the extension of the process language with “guarded recursion”. It appears that such an extension violates the completeness of the Hoare logic. This reveals a remarkable property of Scott's induction rule in the context of non-determinism: only regular recursion allows a completeness result.     

Simulating perfect channels with probabilistic lossy channels

We consider the problem of deciding whether an infinite-state system (expressed as a Markov chain) satisfies a correctness property with probability 1. This problem is, of course, undecidable for general infinite-state systems. We focus our attention on the model of probabilistic lossy channel systems consisting of finite-state processes that communicate over unbounded lossy FIFO channels. Abdulla and Jonsson have shown that safety properties are decidable while progress properties are undecidable for non-probabilistic lossy channel systems. Under assumptions of “sufficiently high” probability of loss, Baier and Engelen have shown how to check whether a property holds of probabilistic lossy channel system with probability 1. In this paper, we consider a model of probabilistic lossy channel systems, where messages can be lost only during send transitions. In contrast to the model of Baier and Engelen, once a message is successfully sent to channel, it can only be removed through a transition which receives the message. We show that checking whether safety properties hold with probability 1 is undecidable for this model. Our proof depends upon simulating a perfect channel, with a high degree of confidence, using lossy channels.     

Generic Trace Theory

Trace semantics has been defined for various non-deterministic systems with different input/output types, or with different types of “non-determinism” such as classical non-determinism (with a set of possible choices) vs. probabilistic non-determinism. In this paper we claim that these various forms of “trace semantics” are instances of a single categorical construction, namely coinduction in a Kleisli category. This claim is based on our main technical result that an initial algebra in the category of sets and functions yields a final coalgebra in the Kleisli category, for monads with a suitable order structure. The proof relies on coincidence of limits and colimits, like in the work of Smyth and Plotkin.     

Towards a theory of mathematical operational semantics

Turi and Plotkin gave a precise mathematical formulation of a notion of structural operational semantics in their paper “Towards a mathematical operational semantics.” Starting from that definition and at the level of generality of that definition, we give a mathematical formulation of some of the basic constructions one makes with structural operational semantics. In particular, given a single-step operational semantics, as is the spirit of their work, one composes transitions and considers streams of transitions in order to study the dynamics induced by the operational semantics. In all their leading examples, it is obvious that one can do that and it is obvious how to do it. But if their definition is to be taken seriously, one needs to be able to make such constructions at the level of generality of their definition rather than case-by-case. So this paper does so for several of the basic constructions associated with structural operational semantics, in particular those required in order to speak of a stream of transitions and hence of dynamics.