Concurrent Kleene Algebra (CKA) is a formalism to study concurrent programs. Like previous Kleene Algebra extensions, developing a correspondence between denotational and operational perspectives is important, both for foundations and for applications. This paper takes an important step towards such a correspondence, by precisely relating bi-Kleene Algebra (BKA), a fragment of CKA, to a novel type of automata called pomset automata (PAs).We show that PAs can implement the BKA semantics of series-parallel rational expressions, and that a class of PAs can be translated back to these expressions. We also characterise the behaviour of general PAs in terms of context-free pomset grammars; consequently, universality, equivalence and series-parallel rationality of general PAs are undecidable. (C) 2018 Elsevier Inc. All rights reserved.
Kappe T., Brunet P., Luttik B., Silva A., Zanasi F. (2019). On series-parallel pomset languages: Rationality, context-freeness and automata. THE JOURNAL OF LOGICAL AND ALGEBRAIC METHODS IN PROGRAMMING, 103, 130-153 [10.1016/j.jlamp.2018.12.001].
On series-parallel pomset languages: Rationality, context-freeness and automata
Brunet P.;Zanasi F.
2019
Abstract
Concurrent Kleene Algebra (CKA) is a formalism to study concurrent programs. Like previous Kleene Algebra extensions, developing a correspondence between denotational and operational perspectives is important, both for foundations and for applications. This paper takes an important step towards such a correspondence, by precisely relating bi-Kleene Algebra (BKA), a fragment of CKA, to a novel type of automata called pomset automata (PAs).We show that PAs can implement the BKA semantics of series-parallel rational expressions, and that a class of PAs can be translated back to these expressions. We also characterise the behaviour of general PAs in terms of context-free pomset grammars; consequently, universality, equivalence and series-parallel rationality of general PAs are undecidable. (C) 2018 Elsevier Inc. All rights reserved.I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.



