Thursday, 4 February 2010, 14:00
Cybernetica Bldg (Akadeemia tee 21), room B101
Slides from the talk [pdf]
Abstract: We present directed bigraphs and directed bigraphical reactive systems, a framework for describing computational models dealing with locations and resource communications. The key novelty is that directed bigraphs take account of the "resource request flow" from controls to edges (through names).
For this model we give the construction for relative pushouts (RPOs). On this basis, directed bigraphs can be used for describing computational models, allowing to synthesised systematically labelled transition systems by means of the so-called RPO construction; notably, the corresponding bisimulations are always congruences. Under mild conditions, these LTSs can be reduced further by restricting to a subclass of labels, which can be characterized syntactically.
In order to demonstrate the encoding methodology, we consider the case of fusion calculus, for which we give a directed bigraphical reactive system and study the resulting labelled transition system and compositional bisimilarity.