Skip to Main content Skip to Navigation
Preprints, Working Papers, ...

Compositional equivalences based on open pNets

Rabea Ameur-Boulifa 1 Ludovic Henrio 2 Eric Madelaine 3
2 SCALE - Safe Composition of Autonomous applications with Large-SCALE Execution environment
Laboratoire I3S - COMRED - COMmunications, Réseaux, systèmes Embarqués et Distribués
3 KAIROS - Logical Time for Formal Embedded System Design
Laboratoire I3S - COMRED - COMmunications, Réseaux, systèmes Embarqués et Distribués, CRISAM - Inria Sophia Antipolis - Méditerranée
Abstract : Establishing equivalences between programs or system 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 relations, allowing some of the actions to be invisible or internal moves, and thus not simulated by the equivalent program. pNets is a generalisation of automata that includes parameters, and hierarchical composition. Open pNets are pNets with holes, i.e. placeholders inside the hierarchical structure that can be filled by subsystems. Reasoning on open pNets allows us to reason on open systems. Open pNets have a notion of synchronised actions generalizing the usual internal actions (e.g. τ of CCS, or i in Lotos). This article defines bisimulation relations for the comparison of systems specified as pNets. We first define a strong bisimulation for open pNets. In practice, as happens in process algebras, strong bisimulation is too strong, and we need to define some coarser relations, taking into account invisible or internal moves. 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. The article is illustrated with a transport protocol running example; it shows the characteristics of our formalism and our bisimulation relations.
Complete list of metadata
Contributor : Eric Madelaine Connect in order to contact the contributor
Submitted on : Friday, January 8, 2021 - 11:28:00 AM
Last modification on : Friday, January 21, 2022 - 3:12:05 AM
Long-term archiving on: : Friday, April 9, 2021 - 6:44:47 PM


Files produced by the author(s)


  • HAL Id : hal-03103607, version 1


Rabea Ameur-Boulifa, Ludovic Henrio, Eric Madelaine. Compositional equivalences based on open pNets. 2021. ⟨hal-03103607⟩



Les métriques sont temporairement indisponibles