Compositional equivalences based on Open pNets

TL;DR

This paper introduces bisimulation relations for open pNets, a hierarchical automata model, enabling compositional equivalence checking of open systems with variables and placeholders.

Contribution

It defines strong and weak bisimulation relations for open pNets and establishes conditions for their compositionality, advancing formal verification methods for open systems.

Findings

Defined strong bisimulation for open pNets.

Introduced a weak bisimulation-like relation for open pNets.

Proved conditions ensuring compositionality of these bisimulations.

Abstract

Establishing equivalences between programs or systems is crucial both for verifying correctness of programs, by establishing that two implementations are equivalent, and for justifying optimisations and program transformations, by establishing that a modified program is equivalent to the source one. There exist several equivalence relations for programs, and bisimulations are among the most versatile of these equivalences. Among bisimulation relations one distinguishes strong bisimulation, that requires that each action of a program is simulated by a single action of the equivalent program, a weak bisimulation that is a coarser relation, allowing some of the actions to be invisible or internal moves, and thus not simulated by the equivalent program. pNet is a generalisation of automata that model open systems. They feature variables and hierarchical composition. Open pNets are pNets with holes, i.e. placeholders inside the hierarchical structure that can be filled later by sub-systems. This article defines bisimulation relations for the comparison of systems specified as pNets. We first define a strong bisimulation for open pNets. We then define an equivalence relation similar to the classical weak bisimulation, and study its properties. Among these properties we are interested in compositionality: if two systems are proven equivalent they will be undistinguishable by their context, and they will also be undistinguishable when their holes are filled with equivalent systems. We identify sufficient conditions on the automata to ensure compositionality of strong and weak bisimulation. The article is illustrated with a transport protocol running example; it shows the characteristics of our formalism and our bisimulation relations.