Groote and Luttik (1998a) proved that the extension of the theory pCRL with the axioms for branching bisimulation of Van Glabbeek and Weijland (1996) yields a ground complete axiomatisation of branching bisimulation algebras with data, and conditionals and alternative quantification over these, provided that the data part has built-in equality and built-in Skolem functions. In this paper we shall use this result to obtain ground complete axiomatisations of $eta$-bisimulation algebras, delay bisimulation algebras and weak bisimulation algebras with data, conditionals and alternative quantification over data, under the same proviso as before. Groote and Luttik (1998a) proved that the extension of the theory pCRL with the axioms for branching bisimulation of Van Glabbeek and Weijland (1996) yields a ground complete axiomatisation of branching bisimulation algebras with data, and conditionals and alternative quantification over these, provided that the data part has built-in equality and built-in Skolem functions. In this paper we shall use this result to obtain ground complete axiomatisations of $eta$-bisimulation algebras, delay bisimulation algebras and weak bisimulation algebras with data, conditionals and alternative quantification over data, under the same proviso as before.

, ,
, , ,
CWI
Software Engineering [SEN]

Luttik, B. (1999). Complete axiomatisations of weak-, delay- and $ eta $ -bisimulation for process algebras with alternative quantification over data. Software Engineering [SEN]. CWI.