Lazy probabilistic model checking without determinisation

Hahn, EM, Li, G, Schewe, S ORCID: 0000-0002-9093-9518, Turrini, A and Zhang, L (2015) Lazy probabilistic model checking without determinisation. In: 26th International Conference on Concurrency Theory (CONCUR 2015). Leibniz International Proceedings in Informatics (LIPIcs), 42 . Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik, pp. 354-367. ISBN 9783939897910

Text
lazy_without_determinisation-short.pdf - Unspecified
Download (618kB)

Official URL: http://drops.dagstuhl.de/opus/volltexte/2015/5391/

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.

Item Type:	Book Section
Depositing User:	Symplectic Admin
Date Deposited:	22 Feb 2017 10:56
Last Modified:	19 Jan 2023 07:19
DOI:	10.4230/LIPIcs.CONCUR.2015.354
Related URLs:	Publisher
URI:	https://livrepository.liverpool.ac.uk/id/eprint/3005475