On Cool Congruence Formats for Weak Bisimulations

Select |




Print


van Glabbeek, Robert

van Glabbeek, Robert


2011-06-20


Journal Article


Theoretical Computer Science


412


28


3283-3302


In TCS 146, Bard Bloom presented rule formats for four main notions of bisimulation with silent moves. He proved that weak bisimulation equivalence is a congruence for any process algebra defined by WB cool rules, and established similar results for rooted weak bisimulation (Milner's "observational congruence"), branching bisimulation and rooted branching bisimulation. This study reformulates Bloom's results in a more accessible form and contributes analogues for (rooted) eta-bisimulation and (rooted) delay bisimulation. Moreover, finite equational axiomatisations of rooted weak bisimulation equivalence are provided that are sound and complete for finite processes in any RWB cool process algebra. These require the introduction of auxiliary operators with lookahead, and an extension of Bloom's formats for this type of operator with lookahead. Finally, a challenge is presented for which Bloom's formats fall short and further improvement is called for.


Concurrency, structural operational semantics, CCS, compositionality, branching bisimulation, weak bisimulation, complete axiomatizations.


http://www.cse.unsw.edu.au/~rvg/pub/cool.pdf


0304-3975


nicta:4141


van Glabbeek, Robert. On Cool Congruence Formats for Weak Bisimulations. Theoretical Computer Science. 2011-06-20; 412(28):3283-3302.



Loading citation data...

Citation counts
(Requires subscription to view)