Automata with generalized Rabin pairs for probabilistic model checking and LTL synthesis

Krishnendu Chatterjee, Andreas Gaiser, Jan Křetínský

Publikation: Beitrag in Buch/Bericht/KonferenzbandKonferenzbeitragBegutachtung

36 Zitate (Scopus)

Abstract

The model-checking problem for probabilistic systems crucially relies on the translation of LTL to deterministic Rabin automata (DRW). Our recent Safraless translation [KE12, GKE12] for the LTL(F,G) fragment produces smaller automata as compared to the traditional approach. In this work, instead of DRW we consider deterministic automata with acceptance condition given as disjunction of generalized Rabin pairs (DGRW). The Safraless translation of LTL(F,G) formulas to DGRW results in smaller automata as compared to DRW. We present algorithms for probabilistic model-checking as well as game solving for DGRW conditions. Our new algorithms lead to improvement both in terms of theoretical bounds as well as practical evaluation. We compare PRISM with and without our new translation, and show that the new translation leads to significant improvements.

OriginalspracheEnglisch
TitelComputer Aided Verification - 25th International Conference, CAV 2013, Proceedings
Seiten559-575
Seitenumfang17
DOIs
PublikationsstatusVeröffentlicht - 2013
Veranstaltung25th International Conference on Computer Aided Verification, CAV 2013 - Saint Petersburg, Russland
Dauer: 13 Juli 201319 Juli 2013

Publikationsreihe

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

Konferenz

Konferenz25th International Conference on Computer Aided Verification, CAV 2013
Land/GebietRussland
OrtSaint Petersburg
Zeitraum13/07/1319/07/13

Fingerprint

Untersuchen Sie die Forschungsthemen von „Automata with generalized Rabin pairs for probabilistic model checking and LTL synthesis“. Zusammen bilden sie einen einzigartigen Fingerprint.

Dieses zitieren