Lazy probabilistic model checking without determinisation

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

Research output: Chapter in Book/Report/Conference proceedingConference contributionAcademicpeer-review

24 Citations (Scopus)
1 Downloads (Pure)

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.

Original languageEnglish
Title of host publication26th International Conference on Concurrency Theory, CONCUR 2015
EditorsLuca Aceto, David de Frutos Escrig
Place of PublicationDagstuhl
PublisherDagstuhl
Pages354-367
Number of pages14
ISBN (Electronic)9783939897910
DOIs
Publication statusPublished - 2015
Externally publishedYes
Event26th International Conference on Concurrency Theory, CONCUR 2015 - Madrid, Spain
Duration: 1 Sep 20154 Sep 2015
Conference number: 26

Publication series

NameLeibniz International Proceedings in Informatics, LIPIcs
PublisherDagstuhl
Volume42
ISSN (Print)1868-8969

Conference

Conference26th International Conference on Concurrency Theory, CONCUR 2015
Abbreviated titleCONCUR
CountrySpain
CityMadrid
Period1/09/154/09/15

Keywords

  • Determinisation
  • Markov decision processes
  • Model checking
  • PLTL

Fingerprint Dive into the research topics of 'Lazy probabilistic model checking without determinisation'. Together they form a unique fingerprint.

Cite this