Bisimilarity Is Not Finitely Based over BPA with Interrupt

This paper shows that bisimulation equivalence does not afford a finite equational axiomatization over the language obtained by enriching Bergstra and Klop’s Basic Process Algebra with the interrupt operator. Moreover, it is shown that the collection of closed equations over this language is also not finitely based. In sharp contrast to these results, the collection of closed equations over the language BPA enriched with the disrupt operator is proven to be finitely based. Key words: Concurrency, process algebra, Basic Process Algebra (BPA), interrupt, disrupt, bisimulation, equational logic, complete axiomatizations, non-finitely based algebras, expressiveness 1991 MSC: 08A70, 03B45, 03C05, 68Q10, 68Q45, 68Q55, 68Q70 Preprint submitted to Elsevier Science 

• Type: Conference
• Year: 2005
• Where: CALCO
• Authors: Luca Aceto, Wan Fokkink, Anna Ingólfsdóttir, Sumit Nain
• Keywords: Basic Process Algebra, CALCO 2005, Closed Equations, finite Equational Axiomatization