On the Axiomatisability of Priority

L. Aceto, T. Chen, W.J. Fokkink, A. Ingólfsdóttir

Research output: Contribution to JournalArticleAcademicpeer-review

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. We prove that, in the presence of an infinite set of actions, bisimulation equivalence has no finite, sound, ground-complete equational axiomatisation 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 axiomatisations using equations with action predicates as conditions. In the presence of an infinite set of actions, it is shown that, in general, bisimulation equivalence has no finite, sound, ground-complete axiomatisation consisting of equations with action predicates as conditions 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 axiomatisation of bisimulation equivalence using equations with action predicates as conditions. © 2008 Cambridge University Press.
Original languageEnglish
Pages (from-to)5-28
JournalMSCS : Mathematical Structures in Computer Science
Volume18
Issue number1
DOIs
Publication statusPublished - 2008

Bibliographical note

DBLP:journals/mscs/AcetoCFI08

Fingerprint

Dive into the research topics of 'On the Axiomatisability of Priority'. Together they form a unique fingerprint.

Cite this