Skip to Main content Skip to Navigation
Conference papers

Symbolic Bisimulation for Open and Parameterized Systems

Zechen Hou 1 Eric Madelaine 2
2 KAIROS - Logical Time for Formal Embedded System Design
CRISAM - Inria Sophia Antipolis - Méditerranée , Laboratoire I3S - COMRED - COMmunications, Réseaux, systèmes Embarqués et Distribués
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, and proved to be a congruence for their composition. But this equivalence was defined for a variant of open automata that are intrinsically infinite, making it unsuitable for algorithmic treatment. We define a new form of equivalence named StrFH-Bisimul-ation, working on finite encodings of OAs. We prove that StrFH-Bisimulation is consistent and complete with respect to the FH-Bisimulation. Then we propose two algorithms to check StrFH-Bisimula-tion: the first one requires a (user-defined) relation between the states of two finite OAs, and checks whether it is a StrFH-Bisimulation. The second one takes two finite OAs as input, and builds a "weakest StrFH-bisimulation" such that their initial states are bisimilar. We prove that this algorithm terminates when the data domains are finite. Both algorithms use an SMT-solver as a basis to solve the proof obligations.
Complete list of metadatas

Cited literature [20 references]  Display  Hide  Download
Contributor : Eric Madelaine <>
Submitted on : Thursday, December 12, 2019 - 8:22:29 AM
Last modification on : Wednesday, October 14, 2020 - 4:22:49 AM
Long-term archiving on: : Friday, March 13, 2020 - 5:38:46 PM


Files produced by the author(s)




Zechen Hou, Eric Madelaine. Symbolic Bisimulation for Open and Parameterized Systems. PEPM 2020 - ACM SIGPLAN Workshop on Partial Evaluation and Program Manipulation, Jan 2020, New-Orleans, United States. ⟨10.1145/3372884.3373161⟩. ⟨hal-02406098⟩



Record views


Files downloads