Conditions in Reactive Systems and in Graph Rewriting (Abstract) Electronic Communications of the EASST Volume 51 (2012) Proceedings of the 5th International Workshop on Petri Nets, Graph Transformation and other Concurrency Formalisms (PNGT 2012) Conditions in Reactive Systems and in Graph Rewriting (Abstract) Barbara König 1 pages Guest Editors: Julia Padberg, Kathrin Hoffmann Managing Editors: Tiziana Margaria, Julia Padberg, Gabriele Taentzer ECEASST Home Page: http://www.easst.org/eceasst/ ISSN 1863-2122 http://www.easst.org/eceasst/ ECEASST Conditions in Reactive Systems and in Graph Rewriting (Abstract) Barbara König1 1Universität Duisburg-Essen Abstract: We introduce conditional reactive systems, by enriching the reactive sys- tems of Leifer and Milner with application conditions. Furthermore we compare to the situation in graph rewriting where application conditions play a major role. Keywords: reactive systems, graph rewriting, application conditions Reactive Systems were introduced by Leifer and Milner [LM00]. They provide a general cat- egorical setting for modelling abstract rewriting: graph transformation systems, process calculi and also Petri nets can be seen as special cases of reactive systems. In [BCKH11] we have shown how to enrich reactive systems with so-called conditions, by lifting nested application conditions from graph rewriting [HP09] to the setting of reactive sys- tems. This serves two purposes: first, we enrich the formalism of reactive systems by adding application conditions for rules; second, it turns out that some constructions for graph trans- formation systems (such as computing weakest preconditions and strongest postconditions and showing local confluence by means of critical pair analysis) can be done elegantly in the more general setting. It can be shown that nested application conditions in graph rewriting can be encoded into conditions for reactive systems, preserving the applicability of rules (see also [Hül10]). Further- more one can show that the construction of weakest preconditions via borrowed context squares instantiates to well-known constructions for graph rewriting (see [Pen09]). Bibliography [BCKH11] H. S. Bruggink, R. Cauderlier, B. König, M. Hülsbusch. Conditional Reactive Sys- tems. In Proc. of FSTTCS ’11. LIPIcs 13. Schloss Dagstuhl – Leibniz Center for Informatics, 2011. [HP09] A. Habel, K.-H. Pennemann. Correctness of high-level transformation systems rela- tive to nested conditions. Mathematical Stuctures in Computer Science 19:245–296, 2009. [Hül10] M. Hülsbusch. Bisimulation Theory for Graph Transformation Systems. In Proc. of the ICGT ’10 (Doctoral Symposium of the International Conference on Graph Transformation). Pp. 391–393. Springer, 2010. LNCS 6372. [LM00] J. J. Leifer, R. Milner. Deriving Bisimulation Congruences for Reactive Systems. In Proc. of CONCUR 2000. Pp. 243–258. Springer, 2000. LNCS 1877. [Pen09] K.-H. Pennemann. Development of Correct Graph Transformation Systems. PhD thesis, Universität Oldenburg, May 2009. 1 / 1 Volume 51 (2012)