D 2016

Limit-Deterministic Büchi Automata for Linear Temporal Logic

SICKERT, Salomon, Javier ESPARZA, Stefan JAAX a Jan KŘETÍNSKÝ

Základní údaje

Originální název

Limit-Deterministic Büchi Automata for Linear Temporal Logic

Autoři

SICKERT, Salomon (276 Německo), Javier ESPARZA (724 Španělsko), Stefan JAAX (276 Německo) a Jan KŘETÍNSKÝ (203 Česká republika, garant, domácí)

Vydání

Switzerland, Computer Aided Verification - 28th International Conference, CAV 2016, od s. 312-332, 21 s. 2016

Nakladatel

Springer

Další údaje

Jazyk

angličtina

Typ výsledku

Stať ve sborníku

Obor

10201 Computer sciences, information science, bioinformatics

Stát vydavatele

Švýcarsko

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/16:00088472

Organizační jednotka

Fakulta informatiky

ISBN

978-3-319-41539-0

ISSN

DOI

http://dx.doi.org/10.1007/978-3-319-41540-6_17

UT WoS

000387731400017

Klíčová slova anglicky

verification; probabilistic model checking; temporal logic; automata; determinism

Štítky

core_A, firank_1, formela-conference

Příznaky

Mezinárodní význam, Recenzováno
Změněno: 1. 6. 2022 12:45, RNDr. Pavel Šmerk, Ph.D.

Anotace

V originále

Limit-deterministic Büchi automata can replace deterministic Rabin automata in probabilistic model checking algorithms, and can be significantly smaller. We present a direct construction from an LTL formula \phi to a limit-deterministic Büchi automaton. The automaton is the combination of a non-deterministic component, guessing the set of eventually true G-subformulas of \phi , and a deterministic component verifying this guess and using this information to decide on acceptance. Contrary to the indirect approach of constructing a non-deterministic automaton for \phi and then applying a semi-determinisation algorithm, our translation is compositional and has a clear logical structure. Moreover, due to its special structure, the resulting automaton can be used not only for qualitative, but also for quantitative verification of MDPs, using the same model checking algorithm as for deterministic automata. This allows one to reuse existing efficient implementations of this algorithm without any modification. Our construction yields much smaller automata for formulas with deep nesting of modal operators and performs at least as well as the existing approaches on general formulas.

Návaznosti

GBP202/12/G061, projekt VaV
Název: Centrum excelence - Institut teoretické informatiky (CE-ITI) (Akronym: CE-ITI)
Investor: Grantová agentura ČR, Centrum excelence - Institut teoretické informatiky
Zobrazeno: 7. 11. 2024 11:49