Process Symmetry in Probabilistic Transducers
Model checking is the process of deciding whether a system satisfies a given specification. Often, when the setting comprises multiple processes, the specifications are over sets of input and output signals that correspond to individual processes. Then, many of the properties one wishes to specify are symmetric with respect to the processes identities. In this work, we consider the problem of deciding whether the given system exhibits symmetry with respect to the processes' identities. When the system is symmetric, this gives insight into the behaviour of the system, as well as allows the designer to use only representative specifications, instead of iterating over all possible process identities.
Specifically, we consider probabilistic systems, and we propose several variants of symmetry. We start with precise symmetry, in which, given a permutation π, the system maintains the exact distribution of permuted outputs, given a permuted inputs. We proceed to study approximate versions of symmetry, including symmetry induced by small L_∞ norm, variants of Parikh-image based symmetry, and qualitative symmetry. For each type of symmetry, we consider the problem of deciding whether a given system exhibits this type of symmetry.
Symmetry
Probabilistic Transducers
Model Checking
Permutations
Theory of computation~Verification by model checking
Theory of computation~Concurrency
Theory of computation~Abstraction
35:1-35:14
Regular Paper
The author thanks Gal Vardi for discussions on the motivation for this work.
Shaull
Almagor
Shaull Almagor
Computer Science Department, Technion, Haifa, Israel
https://orcid.org/0000-0001-9021-1175
Supported by a European Union’s Horizon 2020 research and innovation programme under the Marie Skłodowska-Curie grant agreement No 837327.
10.4230/LIPIcs.FSTTCS.2020.35
Thomas Ball and Orna Kupferman. Vacuity in testing. In International Conference on Tests and Proofs, pages 4-17. Springer, 2008.
Peter J Cameron et al. Permutation groups, volume 45. Cambridge University Press, 1999.
Edmund M. Clarke, Reinhard Enders, Thomas Filkorn, and Somesh Jha. Exploiting symmetry in temporal logic model checking. Formal methods in system design, 9(1-2):77-104, 1996.
Edmund M Clarke Jr, Orna Grumberg, Daniel Kroening, Doron Peled, and Helmut Veith. Model checking. MIT press, 2018.
A Donaldson and Alice Miller. Symmetry reduction for probabilistic systems. In Proc. 12th workshop on Automated Reasoning, pages 17-18, 2005.
E Allen Emerson and A Prasad Sistla. Symmetry and model checking. Formal methods in system design, 9(1-2):105-131, 1996.
Hugo Gimbert and Youssouf Oualhadj. Probabilistic automata on finite words: Decidable and undecidable problems. In International Colloquium on Automata, Languages, and Programming, pages 527-538. Springer, 2010.
C Norris Ip and David L Dill. Better verification through symmetry. Formal methods in system design, 9(1-2):41-75, 1996.
Jui-Yi Kao, Narad Rampersad, and Jeffrey Shallit. On nfas where all states are final, initial, or both. Theoretical Computer Science, 410(47-49):5010-5021, 2009.
Stefan Kiefer and Björn Wachter. Stability and complexity of minimising probabilistic automata. In International Colloquium on Automata, Languages, and Programming, pages 268-279. Springer, 2014.
Marta Kwiatkowska, Gethin Norman, and David Parker. Symmetry reduction for probabilistic model checking. In International Conference on Computer Aided Verification, pages 234-248. Springer, 2006.
Anthony W Lin, Truong Khanh Nguyen, Philipp Rümmer, and Jun Sun. Regular symmetry patterns. In International Conference on Verification, Model Checking, and Abstract Interpretation, pages 455-475. Springer, 2016.
Omid Madani, Steve Hanks, and Anne Condon. On the undecidability of probabilistic planning and related stochastic optimization problems. Artificial Intelligence, 147(1-2):5-34, 2003.
Azaria Paz. Introduction to probabilistic automata. Academic Press, 2014.
Marcel Paul Schützenberger. On the definition of a family of automata. Inf. Control., 4(2-3):245-270, 1961.
A Prasad Sistla, Viktor Gyuris, and E Allen Emerson. Smc: a symmetry-based model checker for verification of safety and liveness properties. ACM Transactions on Software Engineering and Methodology (TOSEM), 9(2):133-166, 2000.
Corinna Spermann and Michael Leuschel. Prob gets nauty: Effective symmetry reduction for b and z models. In 2008 2nd IFIP/IEEE International Symposium on Theoretical Aspects of Software Engineering, pages 15-22. IEEE, 2008.
Wen-Guey Tzeng. A polynomial-time algorithm for the equivalence of probabilistic automata. SIAM Journal on Computing, 21(2):216-227, 1992.
Thomas Wahl and Alastair Donaldson. Replication and abstraction: Symmetry in automated formal verification. Symmetry, 2(2):799-847, 2010.
Shaull Almagor
Creative Commons Attribution 3.0 Unported license
https://creativecommons.org/licenses/by/3.0/legalcode