Symbolic Bisimulation for Open and Parameterized Systems - Archive ouverte HAL Access content directly
Conference Papers Year :

Symbolic Bisimulation for Open and Parameterized Systems

(1) , (2)
1
2

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.
Les automates ouverts (OA) sont des modèles symboliques et paramétrés pour les systèmes concurrents ouverts. Ici,ouvert désigne des systèmes partiellement spécifiés, qui peuvent être instanciés ou assemblés pour construire de plus grands systèmes. Une propriété importante pour de tels systèmes est la "compositionnalité", ce qui signifie que les propriétés logiques et les équivalences peuvent être vérifiées localement et seront préservées par la composition. Dans des travaux antérieurs, une notion d’équivalence nommée FH-Bisimulation a été définie pour les automates ouverts et se révélait être une congruence pour leur composition. Mais cette équivalence a été définie pour une variante des automates ouverts intrinsèquement infinis,ce qui la rend impropre au traitement algorithmique.Nous définissons une nouvelle forme d’équivalence nommée StrFH-Bisimulation, travaillant sur des codages finis des OA. Nous prouvons que la StrFH-Bisimulation est cohérente et complète pour la FH-Bisimulation.Nous proposons ensuite deux algorithmes pour vérifier StrFH-Bisimulation: le premier re-quiert une relation (définie par l’utilisateur) entre les états de deux OA finis, et vérifie s’il s’agit d’une strFH-Bisimulation. La seconde prend deux AO finies en entrée et construit une "StrFH-bisimulation la plus faible" telle que leurs états initiaux soient bisimilaires. Nous prouvons que cet algorithme termine lorsque les domaines de données sont finis. Les deux algorithmes utilisent un solveur SMT comme base pour résoudre les obligations de preuve.
Fichier principal
Vignette du fichier
poplws20pepmmain-p7-p-79d1b9f-43140-final.pdf (996.69 Ko) Télécharger le fichier
Origin : Files produced by the author(s)
Loading...

Dates and versions

hal-02406098 , version 1 (12-12-2019)

Identifiers

Cite

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⟩
78 View
160 Download

Altmetric

Share

Gmail Facebook Twitter LinkedIn More