Product Automata and Process Algebra

We define a model of labelled product systems of automata and explore its connections with process calculi and trace languages. Bisimilarity of labelled product systems is defined using a new definition of bisimulation with renaming. Concurrent µ-expressions are defined to describe labelled product systems. This leads to complete axiomatizations and algorithms for bisimulation and failure equivalence over labelled product systems, and for equality over recognizable trace languages. Process algebra is a large enough field of research to have come out with its own handbook [8], but does not have the wide applicability that a field like automata theory does. Valmari [40] points out that ideas from process algebra can usefully be applied to verification using automata theory. Since there are a few textbooks [4, 36, 14], several monographs (with illustrious authors like Hoare [18] and Milner [28]) and a fine Turing award lecture by Milner [29], that this does not commonly happen s...

• Type: Conference
• Year: 2006
• Where: SEFM
• Authors: Kamal Lodaya
• Keywords: Automata Theory, Failure Equivalence, Labelled Product Systems, SEFM 2006, Software Engineering