Document Open Access Logo

Process Symmetry in Probabilistic Transducers

Author Shaull Almagor

PDF
Thumbnail PDF

File

LIPIcs.FSTTCS.2020.35.pdf
  • Filesize: 0.56 MB
  • 14 pages

Document Identifiers

Author Details

Shaull Almagor
  • Computer Science Department, Technion, Haifa, Israel

Funding

  • Almagor, Shaull: Supported by a European Union’s Horizon 2020 research and innovation programme under the Marie Skłodowska-Curie grant agreement No 837327.

Acknowledgements

The author thanks Gal Vardi for discussions on the motivation for this work.

Cite As Get BibTex

Shaull Almagor. Process Symmetry in Probabilistic Transducers. In 40th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2020). Leibniz International Proceedings in Informatics (LIPIcs), Volume 182, pp. 35:1-35:14, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020) https://doi.org/10.4230/LIPIcs.FSTTCS.2020.35

Abstract

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.

Subject Classification

ACM Subject Classification
  • Theory of computation → Verification by model checking
  • Theory of computation → Concurrency
  • Theory of computation → Abstraction
Keywords
  • Symmetry
  • Probabilistic Transducers
  • Model Checking
  • Permutations

Metrics

  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    0
    PDF Downloads
    0
    Metadata Views

References

  1. Thomas Ball and Orna Kupferman. Vacuity in testing. In International Conference on Tests and Proofs, pages 4-17. Springer, 2008. Google Scholar
  2. Peter J Cameron et al. Permutation groups, volume 45. Cambridge University Press, 1999. Google Scholar
  3. 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. Google Scholar
  4. Edmund M Clarke Jr, Orna Grumberg, Daniel Kroening, Doron Peled, and Helmut Veith. Model checking. MIT press, 2018. Google Scholar
  5. A Donaldson and Alice Miller. Symmetry reduction for probabilistic systems. In Proc. 12th workshop on Automated Reasoning, pages 17-18, 2005. Google Scholar
  6. E Allen Emerson and A Prasad Sistla. Symmetry and model checking. Formal methods in system design, 9(1-2):105-131, 1996. Google Scholar
  7. 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. Google Scholar
  8. C Norris Ip and David L Dill. Better verification through symmetry. Formal methods in system design, 9(1-2):41-75, 1996. Google Scholar
  9. 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. Google Scholar
  10. 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. Google Scholar
  11. 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. Google Scholar
  12. 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. Google Scholar
  13. 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. Google Scholar
  14. Azaria Paz. Introduction to probabilistic automata. Academic Press, 2014. Google Scholar
  15. Marcel Paul Schützenberger. On the definition of a family of automata. Inf. Control., 4(2-3):245-270, 1961. Google Scholar
  16. 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. Google Scholar
  17. 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. Google Scholar
  18. Wen-Guey Tzeng. A polynomial-time algorithm for the equivalence of probabilistic automata. SIAM Journal on Computing, 21(2):216-227, 1992. Google Scholar
  19. Thomas Wahl and Alastair Donaldson. Replication and abstraction: Symmetry in automated formal verification. Symmetry, 2(2):799-847, 2010. Google Scholar
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail
© 2023-2024 Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact