Skip to Main content Skip to Navigation

Symbolic Weak Equivalences: Extension, Algorithms, and Minimization - Extended version

Biyang Wang 1 Eric Madelaine 2 Min Zhang 1
2 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 : Open Automata (OA) are symbolic and parameterized models for open concurrent systems. Here open means partially specified systems, that can be instantiated or assembled to build bigger systems. An important property for such systems is ”compositionality”, meaning that logical properties, and equivalences, can be checked locally, and will be preserved by composition. In previous work, a notion of equivalence named FH-Bisimulation was defined for open-automata, coming with both Strong and Weak flavors, where Weak means ignoring internal moves when they have no effect on the external behavior. Both flavors have been proved to be congruences for the OA’s composition. In this paper, we propose a new definition of (weak) open automata, that is both more expressive for encoding the behavior of parameterised systems, and suitable as a finite encoding of weak OAs. We name these meta open automata (meta-WOA), and provide two algorithms to check their equivalence, either explicitely building the meta-WOAs, or constructing their meta open transitions on-demand. The last strategy has better termination properties. Then we provide pattern-based Reduction rules for OA, and we discuss preservation of Weak FH-Bisimulation by such reductions.
Complete list of metadata
Contributor : Eric Madelaine Connect in order to contact the contributor
Submitted on : Saturday, January 30, 2021 - 10:04:41 PM
Last modification on : Friday, January 21, 2022 - 3:12:30 AM


Files produced by the author(s)


  • HAL Id : hal-03126313, version 1



Biyang Wang, Eric Madelaine, Min Zhang. Symbolic Weak Equivalences: Extension, Algorithms, and Minimization - Extended version. [Research Report] RR-9389, Inria & Université Cote d'Azur, CNRS, I3S, Sophia Antipolis, France; East China Normal University (Shanghai). 2021, pp.71. ⟨hal-03126313⟩



Les métriques sont temporairement indisponibles