A complete equational axiomatization for MPA with string iteration

We study equational axiomatizations of bisimulation equivalence for the language obtained by extending Milner's basic CCS with string iteration. String iteration is a variation on the original binary version of the Kleene star operation p ∗q obtained by restricting the first argument to be a no...

Full description

Saved in:
Bibliographic Details
Published in:Theoretical computer science 1999-01, Vol.211 (1), p.339-374
Main Authors: Aceto, Luca, Groote, Jan Friso
Format: Article
Language:English
Subjects:
Applied sciences
Bisimulation equivalence
Computer science
control theory
systems
Equational logic
Exact sciences and technology
Kleene star
Language theory and syntactical analysis
Minimal process algebra
String iteration
Theoretical computing
Citations: Items that this one cites
Items that cite this one
Online Access:Get full text
Tags: Add Tag
No Tags, Be the first to tag this record!
Description
Summary:We study equational axiomatizations of bisimulation equivalence for the language obtained by extending Milner's basic CCS with string iteration. String iteration is a variation on the original binary version of the Kleene star operation p ∗q obtained by restricting the first argument to be a non-empty sequence of atomic actions. We show that, for every positive integer k, bisimulation equivalence over the set of processes in this language with loops of length at most k is finitely axiomatizable, provided that the set of actions is finite. We also offer an infinite equational theory that completely axiomatizes bisimulation equivalence over the whole language. We prove that this result cannot be improved upon by showing that no finite equational axiomatization of bisimulation equivalence over basic CCS with string iteration can exist, unless the set of actions is empty.
ISSN:0304-3975
1879-2294
DOI:10.1016/S0304-3975(97)00182-5