Symbolic Bisimulation for Open and Parameterized Systems - Extended version

Zechen Hou 1 Eric Madelaine 2 Jing Liu 3, 1
2 OASIS - Active objects, semantics, Internet and security
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

https://hal.inria.fr/hal-02376147
Contributor : Eric Madelaine <>
Submitted on : Friday, November 22, 2019 - 1:35:11 PM
Last modification on : Saturday, November 23, 2019 - 1:39:42 AM

File

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

Identifiers

  • HAL Id : hal-02376147, version 1

Collections

Citation

Zechen Hou, Eric Madelaine, Jing Liu. 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-02376147⟩

Share

Metrics

Record views

46

Files downloads

52