Robin Milner

I&C Journal 2006 Journal Article

Pure bigraphs: Structure and dynamics

• Robin Milner

Bigraphs are graphs whose nodes may be nested, representing locality, independently of the edges connecting them. They may be equipped with reaction rules, forming a bigraphical reactive system (Brs) in which bigraphs can reconfigure themselves. Following an earlier paper describing link graphs, a constituent of bigraphs, this paper is a devoted to pure bigraphs, which in turn underlie various more refined forms. Elsewhere it is shown that behavioural analysis for Petri nets, π-calculus and mobile ambients can all be recovered in the uniform framework of bigraphs. The paper first develops the dynamic theory of an abstract structure, a wide reactive system (Wrs), of which a Brs is an instance. In this context, labelled transitions are defined in such a way that the induced bisimilarity is a congruence. This work is then specialised to Brss, whose graphical structure allows many refinements of the theory. The latter part of the paper emphasizes bigraphical theory that is relevant to the treatment of dynamics via labelled transitions. As a running example, the theory is applied to finite pure CCS, whose resulting transition system and bisimilarity are analysed in detail. The paper also mentions briefly the use of bigraphs to model pervasive computing and biological systems.

CSL Conference 1994 Conference Paper

Higher-Order Action Calculi

• Robin Milner

Abstract Action calculi are a broad class of algebraic structures, including a formulation of Petri nets as well as a formulation of the π -calculus. Each action calculus HAC( K ) is generated by a particular set K of operators called controls. The purpose of this paper is to extend action calculi in a uniform manner to higher-order. A special case is essentially the extension of the π -calculus to higher order by Sangiorgi. To establish a link between the interactive and functional paradigms of computation, a variety of the λ -calculus is obtained as the extension of the smallest action calculus HAC(θ). The dynamics of higher-order action calculi is presented, blending communication -for example in process calculi- with reduction as in the λ -calculus. Strong normalisation is obtained for reduction. A set of equational axioms is given for higher-order action calculi. Taking the quotient of HAC(θ) by a single extra axiom η, a cartesian-closed category is obtained. An ultimate goal of the paper is to combine process calculi and functional calculi, both in their formulation and in their semantics.

MFCS Conference 1993 Invited Paper

Action Calculi, or Syntactic Action Structures

• Robin Milner

Abstract Action structures have previously been proposed as an algebra for both the syntax and the semantics of interactive computation. Here a class of concrete action structures called action calculi is identified, which can serve as a non-linear syntax for a wide variety of models of interactive behaviour. They generalise a previously defined action structure PIC for the π-calculus. One action calculus differs from another only in its generators, called controls. Several extensions to PIC are given as action calculi, giving essentially the same power as the π-calculus. An action calculus is also outlined for PT nets — a class of Petti nets — parametrized upon their places and transitions. Finally, action calculi are characterized as the free algebras in a sub-variety of action structures, namely those which satisfy certain additional axioms.

TCS Journal 1993 Journal Article

Modal logics for mobile processes

• Robin Milner
• Joachim Parrow
• David Walker

In process algebras, bisimulation equivalence is typically defined directly in terms of the operational rules of action; it also has an alternative characterization in terms of a simple modal logic (sometimes called Hennessy-Milner logic). This paper first defines two forms of bisimulation equivalence for the π-calculus, a process algebra which allows dynamic reconfiguration among processes; it then explores a family of possible logics, with different modal operators. It is proven that two of these logics characterize the two bisimulation equivalences. Also, the relative expressive power of all the logics is exhibited as a lattice. The results are applicable to most value-passing process algebras.

TCS Journal 1993 Journal Article

Unique decomposition of processes

• Robin Milner
• Faron Moller

In this paper, we examine questions about the prime decomposability of processes, where we define a process to be prime whenever it cannot be decomposed into nontrivial components. We show that any finite process can be uniquely decomposed into prime processes with respect to bisimulation equivalence, and demonstrate counterexamples to such a result for both failures (testing) equivalence and trace equivalence. Although we show that prime decompositions cannot exist for arbitrary infinite processes, we motivate but leave as open a conjecture on the unique decomposability of a wide subclass of infinite behaviours.

I&C Journal 1992 Journal Article

A calculus of mobile processes, I

• Robin Milner
• Joachim Parrow
• David Walker

We present the π-calculus, a calculus of communicating systems in which one can naturally express processes which have changing structure. Not only may the component agents of a system be arbitrarily linked, but a communication between neighbours may carry information which changes that linkage. The calculus is an extension of the process algebra CCS, following work by Engberg and Nielsen, who added mobility to CCS while preserving its algebraic properties. The π-calculus gains simplicity by removing all distinction between variables and constants; communication links are identified by names, and computation is represented purely as the communication of names across links. After an illustrated description of how the π-calculus generalises conventional process algebras in treating mobility, several examples exploiting mobility are given in some detail. The important examples are the encoding into the π-calculus of higher-order functions (the λ-calculus and combinatory algebra), the transmission of processes as values, and the representation of data structures as processes. The paper continues by presenting the algebraic theory of strong bisimilarity and strong equivalence, including a new notion of equivalence indexed by distinctions—i. e. , assumptions of inequality among names. These theories are based upon a semantics in terms of a labeled transition system and a notion of strong bisimulation, both of which are expounded in detail in a companion paper. We also report briefly on work-in-progress based upon the corresponding notion of weak bisimulation, in which internal actions cannot be observed.

I&C Journal 1992 Journal Article

A calculus of mobile processes, II

• Robin Milner
• Joachim Parrow
• David Walker

This is the second of two papers in which we present the π-calculus, a calculus of mobile processes. We provide a detailed presentation of some of the theory of the calculus developed to date, and in particular we establish most of the results stated in the companion paper.

I&C Journal 1992 Journal Article

A compositional protocol verification using relativized bisimulation

• Kim G. Larsen
• Robin Milner

The purpose of this paper is to illustrate a compositional proof method for communicating systems; that is, a method in which a property P of a complete system is demonstrated by first decomposing the system, then demonstrating properties of the subsystems which are strong enough to entail property P for the complete system. In any compositional proof method, it is essential that one can abstract away the behavioural aspects of the subsystem which are irrelevant in the context of the complete system. Our method is an extension of the well established notion of bisimulation; it is called relative bisimulation, and was developed specifically to allow for such abstractions. We illustrate the method in a proof of correctness for a version of the Alternating Bit Protocol.

TCS Journal 1991 Journal Article

Co-induction in relational semantics

• Robin Milner
• Mads Tofte

An application of the mathematical theory of maximum fixed points of monotonic set operators to relational semantics is presented. It is shown how an important proof method which we call co-induction, a variant of Park's (1969) principle of fixpoint induction, can be used to prove the consistency of the static and the dynamic relational semantics of a small functional programming language with recursive functions.

TCS Journal 1990 Journal Article

Interpreting one concurrent calculus in another

• Robin Milner

I&C Journal 1989 Journal Article

A complete axiomatisation for observational congruence of finite-state behaviours

• Robin Milner

Finite state automata, with non-determinism and silent transitions, can be interpreted not as subsets of the free monoid as in classical automata theory, but as congruence classes under a congruence relation based upon the notion of weak bisimulation or observational equivalence due to Park and Milner. In this paper a complete axiomatisation for this congruence is presented. It extends the previously known complete axiomatisation by Hennessy and Milner for the case when all computations are finite; the extension consists of five simple rules for recursion.

TCS Journal 1983 Journal Article

Calculi for synchrony and asynchrony

• Robin Milner

A calculus for distributed computation is studied, based upon four combinators. A central idea is an Abelian group of actions which models the interfaces between components of a distributed computing agent. Using a notion of bisimulation, congruence relations are defined over computing agents, and thence an algebraic theory is derived. The calculus models both synchronous and asynchronous computation. In particular, it is shown that the author's Calculus of Communicating Systems (1980), which is an asynchronous model, is derivable from the calculus presented here.

MFCS Conference 1979 Invited Paper

LCF: A Way of Doing Proofs with a Machine

• Robin Milner

MFCS Conference 1978 Invited Paper

Synthesis of Communicating Behaviour

• Robin Milner

TCS Journal 1977 Journal Article

Fully abstract models of typed λ-calculi

• Robin Milner

A semantic interpretation A for a programming language L is fully abstract if, whenever A〚C[M]〛⊑A〚C[N]〛 for two program phrases M, N and for all program contexts C [ ], it follows that A〚M〛⊑A〚N〛. A model M for the language is fully abstract if the natural interpretation A of L in M is fully abstract. We show that under certain conditions there exists, for an extended typed λ-calculus, a unique fully abstract model.