James J. Leifer, Robin Milner.
Deriving Bisimulation Congruences for Reactive Systems.
The paper presents a uniform approach for deriving a Labelled Transition System (LTS) semantics from a reduction semantics, in such a way that the resulting bisimilarity is a congruence. LTS semantics, inspired by automata theory, specifies the interactive behaviour of systems, while reduction semantics specifies their internal evolution and is closer to the operational semantics of sequential programs. LTS semantics has been favoured in early work on process calculi, as it lends itself to the definition of a variety of behavioural equivalences that are easy to work with. Subsequently, a wealth of process calculi have been proposed, tailored to specific features (mobility, locations, security, sessions, etc). In these more complex calculi, it became more debatable what to adopt as labels or “observables” for the LTS semantics, and this motivated the shift towards a reduction semantics in conjunction with a structural congruence, allowing for a compact semantic description.
The thrust to retrieve an LTS semantics from a reduction semantics is an important one, and this paper is a milestone in this line of work. The solution proposed is robust, i.e., broadly applicable. It is also mathematically elegant, formulated using the categorical notion of relative pushout (RPO). The paper has spurred a whole trend of research on congruence properties for bisimilarity in which RPOs constitute the key notion. Good examples are applications to bigraphs, graph rewriting and name calculi.
Luca de Alfaro, Marco Faella, Thomas A. Henzinger, Rupak Majumdar, Mariëlle Stoelinga.
The Element of Surprise in Timed Games.
The paper studies concurrent two-player games played on timed game structures, and in particular the ones arising from playing on timed automata. A key contribution of the paper is the definition of an elegant timed game model, allowing both the representation of moves that can take the opponent by surprise as they are played "faster", and the definition of natural concepts of winning conditions for the two players -- ensuring that players can win only by playing according to a physically meaningful strategy. This approach provides a clean answer to the problem of time convergence, and the responsibility of the players in it. For this reason, it has since been the basis of numerous works on timed games. The algorithm established in the paper to study omega-regular conditions in this neat model of timed games is also enticing, resorting to mu-calculus on a cleverly enriched structure.