D 2012

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

KŘETÍNSKÝ, Jan a Javier ESPARZA

Základní údaje

Originální název

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

Autoři

KŘETÍNSKÝ, Jan (203 Česká republika, garant, domácí) a Javier ESPARZA (724 Španělsko)

Vydání

Heidelberg Dordrecht London New York, Computer Aided Verification - 24th International Conference, od s. 7-22, 16 s. 2012

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/12:00057483

Organizační jednotka

Fakulta informatiky

ISBN

978-3-642-31423-0

ISSN

DOI

Klíčová slova anglicky

linear temporal logic; automata; determinism

Štítky

Příznaky

Mezinárodní význam, Recenzováno
Změněno: 22. 4. 2013 23:42, RNDr. Pavel Šmerk, Ph.D.

Anotace

V originále

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.

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
MUNI/A/0758/2011, 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/0914/2009, interní kód MU
Název: Rozsáhlé výpočetní systémy: modely, aplikace a verifikace (Akronym: SV-FI MAV)
Investor: Masarykova univerzita, Rozsáhlé výpočetní systémy: modely, aplikace a verifikace, DO R. 2020_Kategorie A - Specifický výzkum - Studentské výzkumné projekty