Title
Rational Operational Models
Abstract
GSOS is a specification format for well-behaved operations on transition systems. Aceto introduced a restriction of this format, called simple GSOS, which guarantees that the associated transition system is locally finite, i.e. every state has only finitely many different descendent states (i.e. states reachable by a sequence of transitions). The theory of coalgebras provides a framework for the uniform study of systems, including labelled transition systems but also, e.g. weighted transition systems and (non-)deterministic automata. In this context GSOS can be studied at the general level of distributive laws of syntax over behaviour. In the present paper we generalize Aceto@?s result to the setting of coalgebras by restricting abstract GSOS to bipointed specifications. We show that the operational model of a bipointed specification is locally finite, even for specifications with infinitely many operations which have finite dependency. As an example, we derive a concrete format for operations on regular languages and obtain for free that regular expressions have finitely many derivatives modulo the equations of join semilattices.
Year
DOI
Venue
2013
10.1016/j.entcs.2013.09.017
Electr. Notes Theor. Comput. Sci.
Keywords
Field
DocType
finite dependency,rational operational models,bipointed specification,transition system,simple gsos,labelled transition system,weighted transition system,context gsos,concrete format,associated transition system,abstract gsos,distributive law
Transition system,Discrete mathematics,Distributive property,Regular expression,Modulo,Computer science,Automaton,Coalgebra,Regular language,Syntax
Journal
Volume
ISSN
Citations 
298,
1571-0661
0
PageRank 
References 
Authors
0.34
18
4
Name
Order
Citations
PageRank
Stefan Milius151157.28
Marcello M. Bonsangue282466.34
Robert S. R. Myers3364.86
Jurriaan Rot410418.53