Open Automata: Meta Extension And Weak Bisimulation Checking Algorithm

Automata are significant tools for modeling systems,which are also unfailing topics in the academic field.However,facing the larger and more complex modeling target,traditional automata theories meet a great challenge.That's why coming the birth of Open Automata(OA).OA is a symbolic and parameterized model for open concurrent systems.Here'open'means partially specified systems that can be instantiated or assembled to build more extensive systems.In previous work,Open Transition and OA were proposed with both Strong and Weak flavors.A notion of equivalence named FH-Bisimulation(Formal Hypotheses)was defined for OA,coming with two flavors too.The key idea of FH-Bisimulation is that for two given OAs,each one of them simulates the other's behaviors when satisfying some formal hypotheses.However,some problems still waiting to be solved in the OA theories.For example,the construction rules are iterative and in some special structures,the construction process is endless,which means it's hard to present the weak OA in a finite way,and it's also impossible to check the weak FH-Bisimulation in these cases.The topic about OA's minimization and reduction is also unexplored.We introduce meta-Variables to solve the above problems which encode the infinity weak OA in a finite way.Meta-Variables extend the theories of OA with the meta OA and meta FH-Bisimulation,which have better description ability and enrich the OA theories.We provide two strategies to check their equivalence,either explicitly building the complete(meta)OAs,or constructing their weak Open Transitions on-demand.The previous one is complex and the second strategy has better termination properties.So,we define a'Weak StrFH-Bisimulation' for Implementation,and then we design and realize corresponding checking algorithms with SMT solver for relative proof obligation.We also do lots of research about Minimization and Reductions:We propose the‘One State Minimization' and prove it preserves the Strong FH-Bisimulation;We provide pattern-based Reduction rules for OAs,and we discuss preservation of weak FHBisimulation by such reductions with‘local' bisimulation.At last,we use a communication protocol based on unreliable media as an example to show the practicability of our theories.The correctness of the minimization and reduction rules(partial)is proven.