LTL to Smaller Self-Loop Alternating Automata and Back

D 2019

LTL to Smaller Self-Loop Alternating Automata and Back

BLAHOUDEK, František, Juraj MAJOR a Jan STREJČEK

Základní údaje

Originální název

LTL to Smaller Self-Loop Alternating Automata and Back

Autoři

BLAHOUDEK, František (203 Česká republika), Juraj MAJOR (703 Slovensko, domácí) a Jan STREJČEK (203 Česká republika, garant, domácí)

Vydání

Cham (Switzerland), Theoretical Aspects of Computing - ICTAC 2019 - 16th International Colloquium, Hammamet, Tunisia, October 31 - November 4, 2019, Proceedings, od s. 152-171, 20 s. 2019

Nakladatel

Springer

Další údaje

Jazyk

angličtina

Typ výsledku

Stať ve sborníku

Obor

10200 1.2 Computer and information sciences

Stát vydavatele

Švýcarsko

Utajení

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

Forma vydání

elektronická verze "online"

Odkazy

URL

Impakt faktor

Impact factor: 0.402 v roce 2005

Kód RIV

RIV/00216224:14330/19:00107795

Organizační jednotka

Fakulta informatiky

ISBN

978-3-030-32504-6

ISSN

DOI

http://dx.doi.org/10.1007/978-3-030-32505-3_10

UT WoS

000582443200010

Klíčová slova anglicky

LTL; linear temporal logic; automata; automata over infinite words; alternating automata; LTL to automata; ltl3tela

Štítky

alternating automata, automata, core_B, firank_B, formela-conference, linear temporal logic, LTL, omega-automata, 𝜔-automata

Příznaky

Mezinárodní význam, Recenzováno

Změněno: 28. 4. 2020 00:00, RNDr. Pavel Šmerk, Ph.D.

Anotace

V originále

Self-loop alternating automata (SLAA) with Büchi or co-Büchi acceptance are popular intermediate formalisms in translations of LTL to deterministic or nondeterministic automata. This paper considers SLAA with generic transition-based Emerson-Lei acceptance and presents translations of LTL to these automata and back. Importantly, the translation of LTL to SLAA with generic acceptance produces considerably smaller automata than previous translations of LTL to Büchi or co-Büchi SLAA. Our translation is already implemented in the tool LTL3TELA, where it helps to produce small deterministic or nondeterministic automata for given LTL formulae.

Návaznosti

GA19-24397S, projekt VaV

Název: Automaty v rozhodovacích procedurách a verifikaci (Akronym: AUTODEV)

Investor: Grantová agentura ČR, Automata for Decision Procedures and Verification

MUNI/A/1018/2018, interní kód MU

Název: Rozsáhlé výpočetní systémy: modely, aplikace a verifikace VIII.

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

MUNI/A/1040/2018, interní kód MU

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

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

Citovat

BLAHOUDEK, František, Juraj MAJOR a Jan STREJČEK. LTL to Smaller Self-Loop Alternating Automata and Back. Online. In Robert Mark Hierons, Mohamed Mosbah. Theoretical Aspects of Computing - ICTAC 2019 - 16th International Colloquium, Hammamet, Tunisia, October 31 - November 4, 2019, Proceedings. Cham (Switzerland): Springer, 2019, s. 152-171. ISBN 978-3-030-32504-6. Dostupné z: https://dx.doi.org/10.1007/978-3-030-32505-3_10.

@inproceedings{1580376,
   author = {Blahoudek, František and Major, Juraj and Strejček, Jan},
   address = {Cham (Switzerland)},
   booktitle = {Theoretical Aspects of Computing - ICTAC 2019 - 16th International Colloquium, Hammamet, Tunisia, October 31 - November 4, 2019, Proceedings},
   doi = {http://dx.doi.org/10.1007/978-3-030-32505-3_10},
   editor = {Robert Mark Hierons, Mohamed Mosbah},
   keywords = {LTL; linear temporal logic; automata; automata over infinite words; alternating automata; LTL to automata; ltl3tela},
   howpublished = {elektronická verze "online"},
   language = {eng},
   location = {Cham (Switzerland)},
   isbn = {978-3-030-32504-6},
   pages = {152-171},
   publisher = {Springer},
   title = {LTL to Smaller Self-Loop Alternating Automata and Back},
   url = {https://link.springer.com/chapter/10.1007/978-3-030-32505-3_10},
   year = {2019}
}

TY  - JOUR
ID  - 1580376
AU  - Blahoudek, František - Major, Juraj - Strejček, Jan
PY  - 2019
TI  - LTL to Smaller Self-Loop Alternating Automata and Back
PB  - Springer
CY  - Cham (Switzerland)
SN  - 9783030325046
KW  - LTL
KW  - linear temporal logic
KW  - automata
KW  - automata over infinite words
KW  - alternating automata
KW  - LTL to automata
KW  - ltl3tela
UR  - https://link.springer.com/chapter/10.1007/978-3-030-32505-3_10
L2  - https://link.springer.com/chapter/10.1007/978-3-030-32505-3_10
N2  - Self-loop alternating automata (SLAA) with Büchi or co-Büchi acceptance are popular intermediate formalisms in translations of LTL to deterministic or nondeterministic automata. This paper considers SLAA with generic transition-based Emerson-Lei acceptance and presents translations of LTL to these automata and back. Importantly, the translation of LTL to SLAA with generic acceptance produces considerably smaller automata than previous translations of LTL to Büchi or co-Büchi SLAA. Our translation is already implemented in the tool LTL3TELA, where it helps to produce small deterministic or nondeterministic automata for given LTL formulae.
ER  -

BLAHOUDEK, František, Juraj MAJOR a Jan STREJČEK. LTL to Smaller Self-Loop Alternating Automata and Back. Online. In Robert Mark Hierons, Mohamed Mosbah. \textit{Theoretical Aspects of Computing - ICTAC 2019 - 16th International Colloquium, Hammamet, Tunisia, October 31 - November 4, 2019, Proceedings}. Cham (Switzerland): Springer, 2019, s.~152-171. ISBN~978-3-030-32504-6. Dostupné z: https://dx.doi.org/10.1007/978-3-030-32505-3\_{}10.

Podrobný výpis o publikaci