Symbolic Weak Equivalences: Extension, Algorithms, and Minimization - Extended version

Description

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, coming with both Strong and Weak flavors, where Weak means ignoring internal moves when they have no effect on the external behavior. Both flavors have been proved to be congruences for the OA's composition. In this paper, we propose a new definition of (weak) open automata, that is both more expressive for encoding the behavior of parameterised systems, and suitable as a finite encoding of weak OAs. We name these meta open automata (meta-WOA), and provide two algorithms to check their equivalence, either explicitely building the meta-WOAs, or constructing their meta open transitions on-demand. The last strategy has better termination properties. Then we provide pattern-based Reduction rules for OA, and we discuss preservation of Weak FH-Bisimulation by such reductions.

Abstract (French)

Les Automates Ouverts (OA) sont des modèles symboliques et paramétrés pour les systèmes concurrents ouverts. Ici, ouvert signifie des systèmes partiellement spécifiés, qui peuvent être instanciés ou assemblés pour construire des systèmes plus grands. 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 composition. Dans les travaux précédents, une notion d'équivalence nommée FH-Bisimulation a été définie pour les automates ouverts, en deux versions Forte et Faible, où Faible signifie ignorer les mouvements internes des composants du systéme lorsqu'ils n'ont aucun effet sur le comportement externe. Les deux versions se sont avérées être des congruences pour la composition des OAs. Dans cet article, nous proposons une nouvelle définition des automates ouverts (faibles), qui est plus expressive pour coder le comportement des systèmes paramétrés, et qui permet aussi un codage fini des OAs faibles. Nous les nommons meta automates ouverts (meta-WOA), et fournissons deux algorithmes pour vérifier leur équivalence, soit en construisant explicitement les métaWOA, soit en construisant leurs méta-transitions ouvertes à la demande. La dernière stratégie a de meilleures propriétés de terminaison. Ensuite, nous fournissons des règles de réécriture permettant de réduire la taille des OAs, et nous discutons de la préservation de la bisimulation faible par ce type de réductions.

Additional details