Universal axioms for bisimulations (Q685411)

Observation structures as a basic model of concurrent distributed systems are introduced. They are graphs with nodes labelled by observations. In the special case of observation trees their nodes represent computations of systems and the label of a node is an encoding of the observation of the corresponding computation performed from the beginning of the experiment. A partial ordering over observations is assumed since as computations grow, so do their observations. A language for denoting observation trees is proposed and congruences over its terms are defined as strong, rooted branching and rooted weak bisimulations. Also a new bisimulation, called jumping bisimulation, which is weaker then weak bisimulation is defined. In the case of finite observation structures sound and complete axiomatizations for all bisimulations are given. It is claimed that most of the bisimulation-based congruences known in the literature can be recast in terms of congruences on observation structures, by carefully choosing both the bisimulation and the observation domain.