Technical reports

Transition systems, link graphs and Petri nets

James J. Leifer, Robin Milner

August 2004, 64 pages

DOI: 10.48456/tr-598

Abstract

A framework is defined within which reactive systems can be studied formally. The framework is based upon s-categories, 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 upon the notion of relative pushout 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.

Full text

PDF (0.6 MB)

BibTeX record

@TechReport{UCAM-CL-TR-598,
  author =	 {Leifer, James J. and Milner, Robin},
  title = 	 {{Transition systems, link graphs and Petri nets}},
  year = 	 2004,
  month = 	 aug,
  url = 	 {https://www.cl.cam.ac.uk/techreports/UCAM-CL-TR-598.pdf},
  institution =  {University of Cambridge, Computer Laboratory},
  doi = 	 {10.48456/tr-598},
  number = 	 {UCAM-CL-TR-598}
}