Skip to Main content Skip to Navigation
Reports

Symbolic Bisimulation for Open and Parameterized Systems - Extended version

Zechen Hou 1 Eric Madelaine 2, 3 Jing Liu 1 Yuxin Deng 1
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
Résumé : 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-Bisimulationa é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.
Complete list of metadatas

Cited literature [12 references]  Display  Hide  Download

https://hal.inria.fr/hal-02376147
Contributor : Eric Madelaine <>
Submitted on : Thursday, December 12, 2019 - 10:03:37 AM
Last modification on : Thursday, March 5, 2020 - 12:20:51 PM

File

RR-9304.pdf
Files produced by the author(s)

Identifiers

  • HAL Id : hal-02376147, version 2

Collections

Citation

Zechen Hou, Eric Madelaine, Jing Liu, Yuxin Deng. Symbolic Bisimulation for Open and Parameterized Systems - Extended version. [Research Report] RR-9304, Inria & Université Cote d'Azur, CNRS, I3S, Sophia Antipolis, France; East China Normal University (Shanghai). 2019, pp.47. ⟨hal-02376147v2⟩

Share

Metrics

Record views

40

Files downloads

174