TY - GEN
T1 - New Symbolic Model and Equivalences Checking for Open Automata
AU - Wang, Biyang
AU - Madelaine, Eric
AU - Zhang, Min
N1 - Publisher Copyright:
© 2021 IEEE.
PY - 2021
Y1 - 2021
N2 - Open Automata (OA) are symbolic and parameterized models for open concurrent systems, where open means partially specified systems, which can be instantiated or assembled to build bigger systems. In previous work, a notion of equivalence named FH-Bisimulation was defined for OA, coming with both Strong and Weak flavors, where Weak means ignoring internal moves when they do not affect the external behavior. Both flavors have been proven to be congruent for the OA's composition. In this paper, we propose a new definition of (weak) OA, that is both more expressive for encoding the behavior of parameterized systems and suitable as a finite encoding of weak OA. We name this meta (weak) OA and provide two methods to check their equivalence, either explicitly building the meta-WOA, or constructing their meta open transitions on-demand. The last strategy has better termination properties.
AB - Open Automata (OA) are symbolic and parameterized models for open concurrent systems, where open means partially specified systems, which can be instantiated or assembled to build bigger systems. In previous work, a notion of equivalence named FH-Bisimulation was defined for OA, coming with both Strong and Weak flavors, where Weak means ignoring internal moves when they do not affect the external behavior. Both flavors have been proven to be congruent for the OA's composition. In this paper, we propose a new definition of (weak) OA, that is both more expressive for encoding the behavior of parameterized systems and suitable as a finite encoding of weak OA. We name this meta (weak) OA and provide two methods to check their equivalence, either explicitly building the meta-WOA, or constructing their meta open transitions on-demand. The last strategy has better termination properties.
UR - https://www.scopus.com/pages/publications/85124306909
U2 - 10.1109/SMC52423.2021.9658672
DO - 10.1109/SMC52423.2021.9658672
M3 - 会议稿件
AN - SCOPUS:85124306909
T3 - Conference Proceedings - IEEE International Conference on Systems, Man and Cybernetics
SP - 2360
EP - 2367
BT - 2021 IEEE International Conference on Systems, Man, and Cybernetics, SMC 2021
PB - Institute of Electrical and Electronics Engineers Inc.
T2 - 2021 IEEE International Conference on Systems, Man, and Cybernetics, SMC 2021
Y2 - 17 October 2021 through 20 October 2021
ER -