2 November 2004The Equational Theory of the Interrupt Operator
Wan Fokkink, Anna Ingólfsdóttir, Sumit Nain and I recently posted a new BRICS report entitled Bisimilarity is not Finitely Based over BPA with Interrupt (30 pages). The work reported in that paper arose from a reading of an interesting technical report by Jan Bergstra and Jos Baeten on the equational theory and expressiveness of mode transfer operators, viz. Mode transfer in process algebra, Rapport CSR 00-01, Vakgroep Informatica, Technische Universiteit Eindhoven 2000.
In that report, Baeten and Bergstra offer an equational axiomatization of bisimulation equivalence over the extension of the language BPAdelta with the disrupt and interrupt operators. This axiomatization is finite, if so is the underlying set of actions -- a state of affairs that is most pleasing for process algebraists.
However, the axiomatization of bisimulation equivalence offered by Baeten and Bergstra in op. cit. relies on the use of four auxiliary operators -- two per mode transfer operator. Although the use of auxiliary operators in the axiomatization of behavioral equivalences over process description languages has been well established since Bergstra and Klop's axiomatization of parallel composition using the left and communication merge operators, to our mind, a result like the aforementioned one always begs the question whether the use of auxiliary operators is necessary to obtain a finite axiomatization of bisimulation equivalence.
For the case of parallel composition, Moller showed that strong bisimulation equivalence is not finitely based over CCS and PA without the left merge operator. Thus auxiliary operators are necessary to obtain a finite axiomatization of parallel composition. But, is the use of auxiliary operators necessary to give a finite axiomatization of bisimulation equivalence over the language BPA enriched with the mode transfer operators studied by Baeten and Bergstra in the aforementioned paper?
We address the above natural question in our work. In particular, we focus on BPA enriched with the interrupt operator, and show that, in the presence of two distinct actions, bisimulation equivalence is not finitely based over BPA with the interrupt operator. Moreover, we prove that the collection of closed equations over this language is also not finitely based. This result provides some evidence that the use of auxiliary operators in the technical developments presented by Baeten and Bergstra is indeed necessary in order to obtain a finite axiomatization of bisimulation equivalence.
I have developed a keen interest in the equational theory of mode transfer operators, and together with my trusted co-authors am now working on the study of omega-complete axiomatizations for bisimulation equivalence over BPA with the disrupt operator, and related topics. I hope to be able to report on our results on these pages soon.
Yesterday I began a new chapter in my working life by taking up a professorship at the School of Computer Science, Reykjavík University. This is my first posting from the North Atlantic this autumn, and I hope to have time to continue this diary from Reykjavík.
Last modified: Tuesday, 02-Nov-2004 13:33:35 CET.