Deterministic Automata for the (F,G)-fragment of LTL

Logo poskytovatele

Varování

Publikace nespadá pod Filozofickou fakultu, ale pod Fakultu informatiky. Oficiální stránka publikace je na webu muni.cz.
Autoři

KŘETÍNSKÝ Jan ESPARZA Javier

Rok publikování 2012
Druh Článek ve sborníku
Konference Computer Aided Verification - 24th International Conference
Fakulta / Pracoviště MU

Fakulta informatiky

Citace
Doi http://dx.doi.org/10.1007/978-3-642-31424-7_7
Obor Informatika
Klíčová slova linear temporal logic; automata; determinism
Popis When dealing with linear temporal logic properties in the setting of e.g. games or probabilistic systems, one often needs to express them as deterministic omega-automata. In order to translate LTL to deterministic omega-automata, the traditional approach first translates the formula to a non-deterministic Buchi automaton. Then a determinization procedure such as of Safra is performed yielding a deterministic omega-automaton. We present a direct translation of the (F,G)-fragment of LTL into deterministic omega-automata with no determinization procedure involved. Since our approach is tailored to LTL, we often avoid the typically unnecessarily large blowup caused by general determinization algorithms. We investigate the complexity of this translation and provide experimental results and compare them to the traditional method.
Související projekty:

Používáte starou verzi internetového prohlížeče. Doporučujeme aktualizovat Váš prohlížeč na nejnovější verzi.