Lazy probabilistic model checking without determinisation

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

doi:10.4230/LIPIcs.CONCUR.2015.354

Lazy probabilistic model checking without determinisation

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

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution › Academic › peer-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 language	English
Title of host publication	26th International Conference on Concurrency Theory, CONCUR 2015
Editors	Luca Aceto, David de Frutos Escrig
Place of Publication	Dagstuhl
Publisher	Dagstuhl
Pages	354-367
Number of pages	14
ISBN (Electronic)	9783939897910
DOIs	https://doi.org/10.4230/LIPIcs.CONCUR.2015.354
Publication status	Published - 2015
Externally published	Yes
Event	26th International Conference on Concurrency Theory, CONCUR 2015 - Madrid, Spain Duration: 1 Sep 2015 → 4 Sep 2015 Conference number: 26

Publication series

Name	Leibniz International Proceedings in Informatics, LIPIcs
Publisher	Dagstuhl
Volume	42
ISSN (Print)	1868-8969

Conference

Conference	26th International Conference on Concurrency Theory, CONCUR 2015
Abbreviated title	CONCUR
Country	Spain
City	Madrid
Period	1/09/15 → 4/09/15

Keywords

Determinisation
Markov decision processes
Model checking
PLTL

Access to Document

10.4230/LIPIcs.CONCUR.2015.354Licence: CC BY

Hahn2015lazyFinal published version, 601 KBLicence: CC BY

Link to publication in Scopus

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

Cite this

Hahn, E. M., Li, G., Schewe, S., Turrini, A., & Zhang, L. (2015). Lazy probabilistic model checking without determinisation. In L. Aceto, & D. de Frutos Escrig (Eds.), 26th International Conference on Concurrency Theory, CONCUR 2015 (pp. 354-367). (Leibniz International Proceedings in Informatics, LIPIcs; Vol. 42). Dagstuhl. https://doi.org/10.4230/LIPIcs.CONCUR.2015.354

@inproceedings{0b7fdc8622ad41549c8279b1540785cd,

title = "Lazy probabilistic model checking without determinisation",

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{\"u}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 = "Determinisation, Markov decision processes, Model checking, PLTL",

author = "Hahn, {Ernst Moritz} and Guangyuan Li and Sven Schewe and Andrea Turrini and Lijun Zhang",

year = "2015",

doi = "10.4230/LIPIcs.CONCUR.2015.354",

language = "English",

series = "Leibniz International Proceedings in Informatics, LIPIcs",

publisher = "Dagstuhl",

pages = "354--367",

editor = "Luca Aceto and {de Frutos Escrig}, David",

booktitle = "26th International Conference on Concurrency Theory, CONCUR 2015",

address = "Germany",

note = "26th International Conference on Concurrency Theory, CONCUR 2015, CONCUR ; Conference date: 01-09-2015 Through 04-09-2015",

}

Hahn, EM, Li, G, Schewe, S, Turrini, A & Zhang, L 2015, Lazy probabilistic model checking without determinisation. in L Aceto & D de Frutos Escrig (eds), 26th International Conference on Concurrency Theory, CONCUR 2015. Leibniz International Proceedings in Informatics, LIPIcs, vol. 42, Dagstuhl, Dagstuhl, pp. 354-367, 26th International Conference on Concurrency Theory, CONCUR 2015, Madrid, Spain, 1/09/15. https://doi.org/10.4230/LIPIcs.CONCUR.2015.354

Lazy probabilistic model checking without determinisation. / Hahn, Ernst Moritz; Li, Guangyuan; Schewe, Sven; Turrini, Andrea; Zhang, Lijun.

26th International Conference on Concurrency Theory, CONCUR 2015. ed. / Luca Aceto; David de Frutos Escrig. Dagstuhl : Dagstuhl, 2015. p. 354-367 (Leibniz International Proceedings in Informatics, LIPIcs; Vol. 42).

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution › Academic › peer-review

TY - GEN

T1 - Lazy probabilistic model checking without determinisation

AU - Hahn, Ernst Moritz

AU - Li, Guangyuan

AU - Schewe, Sven

AU - Turrini, Andrea

AU - Zhang, Lijun

N1 - Conference code: 26

PY - 2015

Y1 - 2015

N2 - 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.

AB - 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.

KW - Determinisation

KW - Markov decision processes

KW - Model checking

KW - PLTL

UR - http://www.scopus.com/inward/record.url?scp=84958240132&partnerID=8YFLogxK

U2 - 10.4230/LIPIcs.CONCUR.2015.354

DO - 10.4230/LIPIcs.CONCUR.2015.354

M3 - Conference contribution

T3 - Leibniz International Proceedings in Informatics, LIPIcs

SP - 354

EP - 367

BT - 26th International Conference on Concurrency Theory, CONCUR 2015

A2 - Aceto, Luca

A2 - de Frutos Escrig, David

PB - Dagstuhl

CY - Dagstuhl

T2 - 26th International Conference on Concurrency Theory, CONCUR 2015

Y2 - 1 September 2015 through 4 September 2015

ER -