Talk "Mathematical Operational Semantics and Finitary System Behaviour"

by Stefan Milius

Wed, 08 January 2014 at 09:00 am in Theddingworth near Leicester, UK

Joint work with: Marcello Bonsangue, Rob Myers, Jurriaan Rot

Abstract: Structural operational semantics is a popular and widely used framework for defining operational semantics by means of transition system specifications (tss). Syntactic restrictions on the format of tss, such as the GSOS format of Bloom, Istrail and Meyer ensure nice properties of operations specified by a tss (e.g. that bisimilarity is a congruence). In seminal work, Turi and Plotkin showed that tss can be generalized to the category-theoretic setting of distributive laws; in particular, they showed that tss in the GSOS format correspond precisely to distributive laws of a certain kind, formed from a functor S, representing the syntax of operations over a functor F, representing the transition type. This talk concerns a category-theoretic generalization of the "simple GSOS" format of Aceto. We will show that specifications in our generalized simple GSOS format induce operations preserving the behaviour of finite systems of type F; as applications we will see operations on regular languages, regular processes and weighted transition systems. We will also present a generalization of Aceto's theorem, which states that the operational (term) model of a tss is locally finite, i.e. from every state of the model only a finite number of states are reachable by a sequence of transitions. Applying our result to the category of join-semilattices and appropriate functors S and F we obtain as a corollary Brzozowki's result that the number of derivatives of a regular expression is finite modulo the join-semilattice equations.