Talk at IFIP WG1.3 Meeting in Bonas
 
A review of the structured transition system method
and its application to various rewriting formalisms
Andrea Corradini
Diparimento di Informatica, Pisa

In the talk I will firstly briefly review the algebraic semantics of structured transition systems originally presented in [CM92]. Intuitively, a transition system is a graph (two objects and two parallel arrows in the category of sets), while a structured transition system is an internal graph in a category where usually objects have a richer structure than sets. The categorical framework makes easy to generalize the construction of the path category of a graph to the structured (internal) case, provided that the ambient category satisfies mild assumptions.

Many rule based computational formalisms are usually presented by stressing some algebraic structure of the states, but sticking, for the definition of the rewriting mechanism, to a collection of rule and to some matching mechanism. The basic intuition I will stress next is that the matching mechanism can be more elegantly presented by lifting the algebric structure from stats to transitions or rules, presenting therefore the systems as a structured transition system. This intuition is made explicit for example for P/T Petri Nets in [MM90], and for term rewriting in Meseguer's (unconditional) Rewriting Logic. Less obvious was the case of Horn Clause Logic [CA93]. In recent years, other rule based systems have been addressed, including term graph rewriting [CG97], rational term rewriting [CG98], cyclic term graph rewriting [CG98a], graph rewriting [CGH99, Hec98]. The last application led to a generalization of the original theory, moving from 2-categories to double-categories.

 

[CM 92] Corradini, A.  and Montanari, U., An algebraic semantics for structured transition systems and its application to logic programs, TCS 103, 51-106, 1992.

[MM90] Meseguer, J. and Montanari, U. , Petri Nets are Monoids, Information & Computation 88, 105-155, 1990.

[CA93] Corradini, A. and Asperti, A., A Categorical Model for Logic Programs: Indexed Monoidal Categories, in Proceedings REX Workshop, Beekbergen, The Netherlands, June 1992, LNCS 666, Springer Verlag, 1993.

[CG97] Corradini, A. and Gadducci, F., A 2-Categorical Presentation of Term Graph Rewriting, in Proc. Category Theory and Computer Science, LNCS 1290, Springer Verlag, 1997.

[CG98] Corradini, A. and Gadducci, F.,  Rational Term Rewriting, in Proc. Foundations of Software Science and Computation Structures (FoSSaCS 98'), LNCS 1378, 1998.

[CG98a] Corradini, A. and Gadducci, F., Rewriting on cyclic structures, Techincal Report TR-98-05, Dipartimento di Informatica, Pisa,, 1998. Extended abstract in Z. Esik, editor, Fixed Points in Computer Science, satellite workshop of MFCS '98. Full version submitted for publication.

[CGH99] Corradini, A., Grosse-Rhode, M. and Heckel, R., An algebra of graph derivations using finite (co-) limit double theories, in Recent Trends in Algebraic Development Techniques (WADT'98), LNCS 1589, Springer Verlag, 1999.

[Hec98]  Heckel, R., Open Graph Transformation Systems: A New Approach to the Compositional Modelling of Concurrent and Reactive System, PhD Thesis, Technische Universitaet Berlin, 1998.