Automata with Generalized Rabin Pairs for Probabilistic Model
Checking and LTL Synthesis

D 2013

Automata with Generalized Rabin Pairs for Probabilistic Model Checking and LTL Synthesis

CHATTERJEE, Krishnendu, Andreas GAISER a Jan KŘETÍNSKÝ

Základní údaje

Originální název

Automata with Generalized Rabin Pairs for Probabilistic Model Checking and LTL Synthesis

Autoři

CHATTERJEE, Krishnendu (356 Indie), Andreas GAISER (276 Německo) a Jan KŘETÍNSKÝ (203 Česká republika, garant, domácí)

Vydání

Heidelberg Dordrecht London New York, Computer Aided Verification - 25th International Conference, CAV 2013, od s. 559-575, 17 s. 2013

Nakladatel

Springer

Další údaje

Jazyk

angličtina

Typ výsledku

Stať ve sborníku

Obor

10201 Computer sciences, information science, bioinformatics

Stát vydavatele

Německo

Utajení

není předmětem státního či obchodního tajemství

Forma vydání

tištěná verze "print"

Impakt faktor

Impact factor: 0.402 v roce 2005

Kód RIV

RIV/00216224:14330/13:00066041

Organizační jednotka

Fakulta informatiky

ISBN

978-3-642-39798-1

ISSN

DOI

http://dx.doi.org/10.1007/978-3-642-39799-8_37

Klíčová slova anglicky

linear temporal logic; automata; determinism; synthesis; probabilistic model checking

Štítky

core_A, firank_1

Příznaky

Mezinárodní význam, Recenzováno

Změněno: 27. 4. 2014 23:03, RNDr. Pavel Šmerk, Ph.D.

Anotace

V originále

The model-checking problem for probabilistic systems crucially relies on the translation of LTL to deterministic Rabin automata (DRW). Our recent Safraless translation 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.

Návaznosti

GAP202/10/1469, projekt VaV

Název: Formální metody pro analýzu a verifikaci komplexních systémů

Investor: Grantová agentura ČR, Formální metody pro analýzu a verifikaci komplexních systémů

MUNI/A/0739/2012, interní kód MU

Název: Zapojení studentů Fakulty informatiky do mezinárodní vědecké komunity (Akronym: SKOMU)

Investor: Masarykova univerzita, Zapojení studentů Fakulty informatiky do mezinárodní vědecké komunity, DO R. 2020_Kategorie A - Specifický výzkum - Studentské výzkumné projekty

MUNI/A/0760/2012, interní kód MU

Název: Rozsáhlé výpočetní systémy: modely, aplikace a verifikace II. (Akronym: FI MAV II.)

Investor: Masarykova univerzita, Rozsáhlé výpočetní systémy: modely, aplikace a verifikace II., DO R. 2020_Kategorie A - Specifický výzkum - Studentské výzkumné projekty

Citovat

CHATTERJEE, Krishnendu, Andreas GAISER a Jan KŘETÍNSKÝ. Automata with Generalized Rabin Pairs for Probabilistic Model Checking and LTL Synthesis. In Computer Aided Verification - 25th International Conference, CAV 2013. Heidelberg Dordrecht London New York: Springer, 2013, s. 559-575. ISBN 978-3-642-39798-1. Dostupné z: https://dx.doi.org/10.1007/978-3-642-39799-8_37.

@inproceedings{1091149,
   author = {Chatterjee, Krishnendu and Gaiser, Andreas and Křetínský, Jan},
   address = {Heidelberg Dordrecht London New York},
   booktitle = {Computer Aided Verification - 25th International Conference, CAV 2013},
   doi = {http://dx.doi.org/10.1007/978-3-642-39799-8_37},
   keywords = {linear temporal logic; automata; determinism; synthesis; probabilistic model checking},
   howpublished = {tištěná verze "print"},
   language = {eng},
   location = {Heidelberg Dordrecht London New York},
   isbn = {978-3-642-39798-1},
   pages = {559-575},
   publisher = {Springer},
   title = {Automata with Generalized Rabin Pairs for Probabilistic Model Checking and LTL Synthesis},
   year = {2013}
}

TY  - JOUR
ID  - 1091149
AU  - Chatterjee, Krishnendu - Gaiser, Andreas - Křetínský, Jan
PY  - 2013
TI  - Automata with Generalized Rabin Pairs for Probabilistic Model Checking and LTL Synthesis
PB  - Springer
CY  - Heidelberg Dordrecht London New York
SN  - 9783642397981
KW  - linear temporal logic
KW  - automata
KW  - determinism
KW  - synthesis
KW  - probabilistic model checking
N2  - The model-checking problem for probabilistic systems crucially relies on the translation of LTL to deterministic Rabin automata (DRW). Our recent Safraless translation 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.
ER  -

CHATTERJEE, Krishnendu, Andreas GAISER a Jan KŘETÍNSKÝ. Automata with Generalized Rabin Pairs for Probabilistic Model Checking and LTL Synthesis. In \textit{Computer Aided Verification - 25th International Conference, CAV 2013}. Heidelberg Dordrecht London New York: Springer, 2013, s.~559-575. ISBN~978-3-642-39798-1. Dostupné z: https://dx.doi.org/10.1007/978-3-642-39799-8\_{}37.

Podrobný výpis o publikaci