Expressiveness modulo bisimilarity of regular expressions with parallel composition

DOI10.1017/S0960129514000309MaRDI QIDQ2971071zbMATH OpenFDO

Authors Bas Luttik, Tim M. Müller, Paul van Tilburg, Jos C. M. Baeten

Publication date 4 April 2017

Published in Mathematical Structures in Computer Science (Search for Journal in Brave)

Full work available at URL https://arxiv.org/abs/1011.6429

Mathematics Subject Classification ID

Formal languages and automata (68Q45) Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.) (68Q85)

Abstract: The languages accepted by finite automata are precisely the languages denoted by regular expressions. In contrast, finite automata may exhibit behaviours that cannot be described by regular expressions up to bisimilarity. In this paper, we consider extensions of the theory of regular expressions with various forms of parallel composition and study the effect on expressiveness. First we prove that adding pure interleaving to the theory of regular expressions strictly increases its expressiveness up to bisimilarity. Then, we prove that replacing the operation for pure interleaving by ACP-style parallel composition gives a further increase in expressiveness. Finally, we prove that the theory of regular expressions with ACP-style parallel composition and encapsulation is expressive enough to express all finite automata up to bisimilarity. Our results extend the expressiveness results obtained by Bergstra, Bethke and Ponse for process algebras with (the binary variant of) Kleene's star operation.

Recommendations

• scientific article; zbMATH DE number 7315073
• A characterization of regular expressions under bisimulation
• On expressive power of regular expressions over infinite orders
• An Equational Axiomatization of Bisimulation over Regular Expressions
• Pattern expressions and pattern automata

Cites work

• scientific article; zbMATH DE number 42752 (Why is no real title available?)
• A complete inference system for a class of regular behaviours
• Branching time and abstraction in bisimulation semantics
• Process algebra for synchronous communication
• The algebra of communicating processes with empty process
• Towards a unified approach to encodability and separation results for process calculi

Cited in

(13)

• Natural projection as partial model checking
• Parallel pushdown automata and commutative context-free grammars in bisimulation semantics (extended abstract)
• A characterization of regular expressions under bisimulation
• scientific article; zbMATH DE number 7315073 (Why is no real title available?)
• A Decision Procedure for Bisimilarity of Generalized Regular Expressions
• A complete proof system for 1-free regular expressions modulo bisimilarity
• Sequential value passing yields a Kleene theorem for processes
• Sequential composition in the presence of intermediate termination (extended abstract)
• The \(\pi\)-calculus is behaviourally complete and orbit-finitely executable
• Sequencing and intermediate acceptance: Axiomatisation and decidability of bisimilarity
• scientific article; zbMATH DE number 7379295 (Why is no real title available?)
• scientific article; zbMATH DE number 7407791 (Why is no real title available?)
• Pushdown Automata and Context-Free Grammars in Bisimulation Semantics

This page was built for publication: Expressiveness modulo bisimilarity of regular expressions with parallel composition

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2971071)