UNIVERSAL AXIOMS FOR BISIMULATIONS

Node-labelled graphs, called observation structures, are introduced as a basic model of concurrent distributed systems and as a framework for dealing with observational equivalences over them. In the special case of observation trees, the nodes represent the computations of a system and are labelled by what is observed out of them. The labelling function parametrically maps into different observation domains, e.g., sequences of actions, partial ordering, mixed ordering, ... 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, is defined which naturally arises in the framework of state-labelled structures. Sound and complete axiomatizations, which are independent of the chosen observations, are exhibited for all bisimulations. It is claimed that most of the bisimulation-based congruences known in the literature, for a given process description language, can be recast in terms of congruences on observation structures, by carefully choosing both the bisimulation and the observation domain. Thus, the process of defining the extensional semantics of a process description language can be factorized into a few stages, for each of which several alternatives with clean rationales are available.