Symbolic Bisimulation for Open and Parameterized Systems - Extended version - Archive ouverte HAL Access content directly
Reports (Research Report) Year : 2019

Symbolic Bisimulation for Open and Parameterized Systems - Extended version

Bisimulation symbolique pour les systèmes ouverts et paramétrés - Version étendue

(1) , (2, 3) , (1) , (1)
1
2
3

Abstract

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.
Fichier principal
Vignette du fichier
RR-9304.pdf (1.08 Mo) Télécharger le fichier
Origin : Files produced by the author(s)
Loading...

Dates and versions

hal-02376147 , version 1 (22-11-2019)
hal-02376147 , version 2 (12-12-2019)

Identifiers

  • HAL Id : hal-02376147 , version 2

Cite

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⟩
112 View
101 Download

Share

Gmail Facebook Twitter LinkedIn More