Robin Milner

Joint Express-Infinity-SOS invited speaker

Bigraphs, multi-local names and confluence

The first test of bigraphs has been on the uniform generation of labelled transition systems (LTSs) whose labels are simple contexts. More recently they are being explored as a way of describing and programming realistic systems, which often involve movement in physical space as well as in the virtual space of (collections of) programs. In this talk I explain two aspects of such work.

First, we need to explore how names can have a definite scope, but still allow useful forms of mobility. In pure bigraphs all names are global (unlimited scope); in local bigraphs, all names are local (ocnfined to one or more regions). One may need a combination of local and global names, but we should first clarify the expressive power of local names alone.

Second, an important aspect of dynamics --at least as important as LTSs-- is the study of confluent reactive systems. Real systems are likely to resolve into confluent and non-confluent parts. We would therefore like to extend techniques for handling confluence (e.g. in lambda calculus) to the more unruly domain of bigraphs. It is strictly more unruly: for example, redexes are no longer either independent or nested; they can intertwine!

In this talk, I shall

1. introduce local bigraphs and some new operations upon them;
2. give general conditions which guarantee weak confluence in a bigraphical reactive system, illustrating them for a simple encoding of lambda calculus (which indeed satisfies them).

I shall also ask: are bigraphs amenable to methods (such as the finiteness of developments) that strengthen weak confluence? If so, then work on the lambda calculus finds a new sphere of application.

Hagen Völzer

Express invited speaker

When a system is fairly correct

Fairness is a convenient and popular tool when modelling and specifying concurrent systems. A large variety of fairness notions exists in the literature. However, in contrast to safety and liveness, there was no fully satisfactory abstract characterisation of fairness.

We give and justify a characterisation of fairness that is in line with the characterisations of safety and liveness given by Lamport, Alpern, and Schneider. We provide independent characterisations in terms of language-theory, game theory, and general topology.

Our characterisation of fairness gives rise to a notion of a "fairly correct" system: a system is fairly correct if there exists a --possibly strong--fairness assumption under which it is correct. Many distributed, especially fault-tolerant, systems are only fairly correct with respect to their actual specification since often, fully correct solutions are too expensive or do not exist.

We motivate this relaxation of correctness and compare it with the probabilistic notion of an "almost correct" system, that is, a system that is correct with probability 1 for a given probability measure. While the two notions "fairly correct" and "almost correct" share many properties, they do not coincide in general.

The comparison of the two notions directly leads to pleasing results for the problem of automatically checking whether a finite-state system is fairly correct.