Document Open Access Logo

Lazy Probabilistic Model Checking without Determinisation

Authors Ernst Moritz Hahn, Guangyuan Li, Sven Schewe, Andrea Turrini, Lijun Zhang

PDF
Thumbnail PDF

File

LIPIcs.CONCUR.2015.354.pdf
  • Filesize: 0.58 MB
  • 14 pages

Document Identifiers

Author Details

Ernst Moritz Hahn
Guangyuan Li
Sven Schewe
Andrea Turrini
Lijun Zhang

Cite AsGet BibTex

Ernst Moritz Hahn, Guangyuan Li, Sven Schewe, Andrea Turrini, and Lijun Zhang. Lazy Probabilistic Model Checking without Determinisation. In 26th International Conference on Concurrency Theory (CONCUR 2015). Leibniz International Proceedings in Informatics (LIPIcs), Volume 42, pp. 354-367, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2015)
https://doi.org/10.4230/LIPIcs.CONCUR.2015.354

Abstract

The bottleneck in the quantitative analysis of Markov chains and Markov decision processes against specifications given in LTL or as some form of nondeterministic Büchi automata is the inclusion of a determinisation step of the automaton under consideration. In this paper, we show that full determinisation can be avoided: subset and breakpoint constructions suffice. We have implemented our approach - both explicit and symbolic versions - in a prototype tool. Our experiments show that our prototype can compete with mature tools like PRISM.
Keywords
  • Markov decision processes
  • model checking
  • PLTL
  • determinisation

Metrics

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

References

  1. Tomás Babiak, Mojmír Kretínský, Vojtech Rehák, and Jan Strejcek. LTL to Büchi automata translation: Fast and more deterministic. In TACAS, volume 7214 of LNCS, pages 95-109, 2012. Google Scholar
  2. Christel Baier and Joost-Pieter Katoen. Principles of Model Checking. MIT Press, 2008. Google Scholar
  3. Andrea Bianco and Luca de Alfaro. Model checking of probabalistic and nondeterministic systems. In FSTTCS, volume 1026 of LNCS, pages 499-513, 1995. Google Scholar
  4. Krishnendu Chatterjee, Andreas Gaiser, and Jan Kretínský. Automata with generalized Rabin pairs for probabilistic model checking and LTL synthesis. In CAV, volume 8044 of LNCS, pages 559-575, 2013. Google Scholar
  5. Frank Ciesinski and Christel Baier. LiQuor: A tool for qualitative and quantitative linear time analysis of reactive systems. In QEST, pages 131-132, 2006. Google Scholar
  6. Costas Courcoubetis and Mihalis Yannakakis. The complexity of probabilistic verification. JACM, 42(4):857-907, 1995. Google Scholar
  7. Alexandre Duret-Lutz. LTL translation improvements in SPOT. In VECoS, pages 72-83, 2011. Google Scholar
  8. Javier Esparza and Jan Kretínský. From LTL to deterministic automata: A Safraless compositional approach. In CAV, volume 8559 of LNCS, pages 192-208, 2014. Google Scholar
  9. Ernst Moritz Hahn, Guangyuan Li, Sven Schewe, Andrea Turrini, and Lijun Zhang. Lazy determinisation for quantitative model checking. CoRR, available at http://arxiv.org/abs/1311.2928, 2014.
  10. Ernst Moritz Hahn, Yi Li, Sven Schewe, Andrea Turrini, and Lijun Zhang. IscasMC: A web-based probabilistic model checker. In FM, volume 8442 of LNCS, pages 312-317, 2014. Google Scholar
  11. Hans Hansson and Bengt Jonsson. A logic for reasoning about time and reliability. FAC, 6(5):512-535, 1994. Google Scholar
  12. Boudewijn R. Haverkort, Holger Hermanns, and Joost-Pieter Katoen. On the use of model checking techniques for dependability evaluation. In SRDS, pages 228-237, 2000. Google Scholar
  13. Zuzana Komárková and Jan Kretínský. Rabinizer 3: Safraless translation of LTL to small deterministic automata. In ATVA, volume 8837 of LNCS, pages 235-241, 2014. Google Scholar
  14. Orna Kupferman, Nir Piterman, and Moshe Y. Vardi. Safraless compositional synthesis. In CAV, volume 4144 of LNCS, pages 31-44, 2006. Google Scholar
  15. Marta Kwiatkowska, Gethin Norman, and David Parker. PRISM 4.0: Verification of probabilistic real-time systems. In CAV, volume 6806 of LNCS, pages 585-591, 2011. Google Scholar
  16. Nir Piterman. From nondeterministic Büchi and Streett automata to deterministic parity automata. JLMCS, 3(3:5), 2007. Google Scholar
  17. Shmuel Safra. On the complexity of ω-automata. In FOCS, pages 319-327, 1988. Google Scholar
  18. Sven Schewe. Tighter bounds for the determinisation of Büchi automata. In FoSSaCS, volume 5504 of LNCS, pages 167-181, 2009. Google Scholar
  19. Sven Schewe and Thomas Varghese. Tight bounds for the determinisation and complementation of generalised Büchi automata. In ATVA, volume 7561 of LNCS, pages 42-56, 2012. Google Scholar
  20. Moshe Y. Vardi and Pierre Wolper. An automata-theoretic approach to automatic program verification (preliminary report). In LICS, pages 332-344, 1986. 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 Imprint Privacy Contact