Open AccessOn the Axiomatizability of Priority
Author(s) -
Luca Aceto,
Taolue Chen,
Wan Fokkink,
Anna Ingólfsdóttir
Publication year - 2006
Publication title -
brics report series
Language(s) - English
Resource type - Journals
eISSN - 1601-5355
pISSN - 0909-0878
DOI - 10.7146/brics.v13i1.21907
Subject(s) - bisimulation , equivalence (formal languages) , mathematics , process calculus , equational logic , operator (biology) , set (abstract data type) , algebra over a field , discrete mathematics , pure mathematics , computer science , theoretical computer science , rewriting , programming language , biochemistry , chemistry , repressor , transcription factor , gene
This paper studies the equational theory of bisimulation equivalence over the process algebra BCCSP extended with the priority operator of Baeten, Bergstra and Klop. It is proven that, in the presence of an infinite set of actions, bisimulation equivalence has no finite, sound, ground-complete equational axiomatization over that language. This negative result applies even if the syntax is extended with an arbitrary collection of auxiliary operators, and motivates the study of axiomatizations using conditional equations. In the presence of an infinite set of actions, it is shown that, in general, bisimulation equivalence has no finite, sound, ground-complete axiomatization consisting of conditional equations over the language studied in this paper. Finally, sufficient conditions on the priority structure over actions are identified that lead to a finite, ground-complete axiomatization of bisimulation equivalence using conditional equations.