Symbolic bisimulation for open and parameterized systems

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, and proved to be a congruence for their composition. But this equivalence was defined for a variant of open-automata that are intrinsically infinite, making it unsuitable for algorithmic treatment. We define a new form of equivalence named StrFH-Bisimulation, working on finite encodings of OAs. We prove that StrFH-Bisimulation is consistent and complete with respect to the FH-Bisimulation. Then we propose two algorithms to check StrFH-Bisimulation: the first one requires a (user-defined) relation between the states of two finite OAs, and checks whether it is a StrFH-Bisimulation. The second one takes two finite OAs as input, and builds a ”weakest StrFH-bisimulation” such that their initial states are bisimilar. We prove that this algorithm terminates when the data domains are finite. Both algorithms use an SMT-solver as a basis to solve the proof obligations.