|
On the Axiomatizability of Priority
Luca Aceto
January 2006 |
Abstract:
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
Available as PostScript, PDF, DVI. |