Transition systems, link graphs and Petri nets

James J. Leifer, Robin Milner

Research output: Contribution to journalArticlepeer-review

Abstract / Description of output

A framework is defined within which reactive systems can be studied formally. The framework is based on s-categories, which are a new variety of categories within which reactive systems can be set up in such a way that labelled transition systems can be uniformly extracted. These lead in turn to behavioural preorders and equivalences, such as the failures preorder (treated elsewhere) and bisimilarity, which are guaranteed to be congruential. The theory rests on the notion of relative pushout, which was previously introduced by the authors.

The framework is applied to a particular graphical model, known as link graphs, which encompasses a variety of calculi for mobile distributed processes. The specific theory of link graphs is developed. It is then applied to an established calculus, namely condition-event Petri nets.

In particular, a labelled transition system is derived for condition-event nets, corresponding to a natural notion of observable actions in Petri-net theory. The transition system yields a congruential bisimilarity coinciding with one derived directly from the observable actions. This yields a calibration of the general theory of reactive systems and link graphs against known specific theories.
Original languageEnglish
Pages (from-to)989-1047
Number of pages59
JournalMathematical Structures in Computer Science
Issue number6
Publication statusPublished - 2006


Dive into the research topics of 'Transition systems, link graphs and Petri nets'. Together they form a unique fingerprint.

Cite this