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

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.