MoChiBA: Probabilistic LTL model checking using limit-deterministic büchi automata

Salomon Sickert, Jan Křetínský

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

15 Scopus citations

Abstract

The limiting factor for quantitative analysis of Markov decision processes (MDP) against specifications given in linear temporal logic (LTL) is the size of the generated product. As recently shown, a special subclass of limit-deterministic Büchi automata (LDBA) can replace deterministic Rabin automata in quantitative probabilistic model checking algorithms. We present an extension of PRISM for LTL model checking of MDP using LDBA. While existing algorithms can be used only with minimal changes, the new approach takes advantage of the special structure and the smaller size of the obtained LDBA to speed up the model checking. We demonstrate the speed up experimentally by a comparison with other approaches.

Original languageEnglish
Title of host publicationAutomated Technology for Verification and Analysis - 14th International Symposium, ATVA 2016, Proceedings
EditorsCyrille Artho, Doron Peled, Axel Legay
PublisherSpringer Verlag
Pages130-137
Number of pages8
ISBN (Print)9783319465197
DOIs
StatePublished - 2016
Event14th International Symposium on Automated Technology for Verification and Analysis, ATVA 2016 - Chiba, Japan
Duration: 17 Oct 201620 Oct 2016

Publication series

NameLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume9938 LNCS
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349

Conference

Conference14th International Symposium on Automated Technology for Verification and Analysis, ATVA 2016
Country/TerritoryJapan
CityChiba
Period17/10/1620/10/16

Fingerprint

Dive into the research topics of 'MoChiBA: Probabilistic LTL model checking using limit-deterministic büchi automata'. Together they form a unique fingerprint.

Cite this