We deal in this paper with some possible connections in between causality based models –and causality based equivalences– for process algebraic terms and automatic verification. To this end we focus on the class of static networks of processes –which we call here “rational”–, which is a safe subclass to ensure finiteness of representation. We introduce successive equivalent models for such terms, heading towards an ever more causal formulation of behaviour control. In the end we rely on (syntactic, recurring) events as the primary behaviour element of our last model. On events we define a bisimulation-like equivalence, with a simple formulation. To ensure correctness and consistency of our equivalence we want to restrict to the reachable part of the structure, and the reachables causes. This is the main topic of actual semantic analysis, and requires building as auxiliary information a rather large set of event prints, or distributed vectors of events last perceived locally. This sadly compares to the distributed vectors of states last reached locally, which make up the (interleaved semantics) automaton. Still, it is finite and suffices to provide an equivalence in some respect more insightful than traditional bisimulation, at least in our restricted rational framework.
Download Full PDF Version (Non-Commercial Use)