ltl3tela: LTL to Small Deterministic or Nondeterministic
Emerson-Lei Automata

D 2019

ltl3tela: LTL to Small Deterministic or Nondeterministic Emerson-Lei Automata

MAJOR, Juraj, František BLAHOUDEK, Jan STREJČEK, Miriama JÁNOŠOVÁ, Tatiana ZBONČÁKOVÁ et. al.

Základní údaje

Originální název

ltl3tela: LTL to Small Deterministic or Nondeterministic Emerson-Lei Automata

Autoři

MAJOR, Juraj (703 Slovensko, domácí), František BLAHOUDEK (203 Česká republika), Jan STREJČEK (203 Česká republika, garant, domácí), Miriama JÁNOŠOVÁ (703 Slovensko, domácí) a Tatiana ZBONČÁKOVÁ (703 Slovensko, domácí)

Vydání

Cham (Switzerland), Automated Technology for Verification and Analysis - 17th International Symposium, ATVA 2019, Taipei, Taiwan, October 28-31, 2019, Proceedings, od s. 357-365, 9 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:00107770

Organizační jednotka

Fakulta informatiky

ISBN

978-3-030-31783-6

ISSN

DOI

http://dx.doi.org/10.1007/978-3-030-31784-3_21

UT WoS

000723515700021

Klíčová slova anglicky

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

Štítky

automata, core_A, firank_A, formela-conference, linear temporal logic, LTL, Model checking, omega-automata

Příznaky

Mezinárodní význam, Recenzováno

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

Anotace

V originále

The paper presents a new tool ltl3tela translating LTL to deterministic or nondeterministic transition-based Emerson-Lei automata (TELA). Emerson-Lei automata use generic acceptance formulae with basic terms corresponding to Büchi and co-Büchi acceptance. The tool combines algorithms of Spot library, a new translation of LTL to TELA via alternating automata, a pattern-based automata reduction method, and few other heuristics. Experimental evaluation shows that ltl3tela can produce deterministic automata that are, on average, noticeably smaller than deterministic TELA produced by state-of-the-art translators Delag, Rabinizer 4, and Spot. For nondeterministic automata, the improvement over Spot is smaller, but still measurable.

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

MAJOR, Juraj, František BLAHOUDEK, Jan STREJČEK, Miriama JÁNOŠOVÁ a Tatiana ZBONČÁKOVÁ. ltl3tela: LTL to Small Deterministic or Nondeterministic Emerson-Lei Automata. Online. In Yu-Fang Chen, Chih-Hong Cheng, Javier Esparza. Automated Technology for Verification and Analysis - 17th International Symposium, ATVA 2019, Taipei, Taiwan, October 28-31, 2019, Proceedings. Cham (Switzerland): Springer, 2019, s. 357-365. ISBN 978-3-030-31783-6. Dostupné z: https://dx.doi.org/10.1007/978-3-030-31784-3_21.

@inproceedings{1577339,
   author = {Major, Juraj and Blahoudek, František and Strejček, Jan and Jánošová, Miriama and Zbončáková, Tatiana},
   address = {Cham (Switzerland)},
   booktitle = {Automated Technology for Verification and Analysis - 17th International Symposium, ATVA 2019, Taipei, Taiwan, October 28-31, 2019, Proceedings},
   doi = {http://dx.doi.org/10.1007/978-3-030-31784-3_21},
   editor = {Yu-Fang Chen, Chih-Hong Cheng, Javier Esparza},
   keywords = {ltl3tela; LTL; linear temporal logic; automata; automata over infinite words; LTL to automata},
   howpublished = {elektronická verze "online"},
   language = {eng},
   location = {Cham (Switzerland)},
   isbn = {978-3-030-31783-6},
   pages = {357-365},
   publisher = {Springer},
   title = {ltl3tela: LTL to Small Deterministic or Nondeterministic Emerson-Lei Automata},
   url = {https://link.springer.com/chapter/10.1007/978-3-030-31784-3_21},
   year = {2019}
}

TY  - JOUR
ID  - 1577339
AU  - Major, Juraj - Blahoudek, František - Strejček, Jan - Jánošová, Miriama - Zbončáková, Tatiana
PY  - 2019
TI  - ltl3tela: LTL to Small Deterministic or Nondeterministic Emerson-Lei Automata
PB  - Springer
CY  - Cham (Switzerland)
SN  - 9783030317836
KW  - ltl3tela
KW  - LTL
KW  - linear temporal logic
KW  - automata
KW  - automata over infinite words
KW  - LTL to automata
UR  - https://link.springer.com/chapter/10.1007/978-3-030-31784-3_21
L2  - https://link.springer.com/chapter/10.1007/978-3-030-31784-3_21
N2  - The paper presents a new tool ltl3tela translating LTL to deterministic or nondeterministic transition-based Emerson-Lei automata (TELA). Emerson-Lei automata use generic acceptance formulae with basic terms corresponding to Büchi and co-Büchi acceptance. The tool combines algorithms of Spot library, a new translation of LTL to TELA via alternating automata, a pattern-based automata reduction method, and few other heuristics. Experimental evaluation shows that ltl3tela can produce deterministic automata that are, on average, noticeably smaller than deterministic TELA produced by state-of-the-art translators Delag, Rabinizer 4, and Spot. For nondeterministic automata, the improvement over Spot is smaller, but still measurable.
ER  -

MAJOR, Juraj, František BLAHOUDEK, Jan STREJČEK, Miriama JÁNOŠOVÁ a Tatiana ZBONČÁKOVÁ. ltl3tela: LTL to Small Deterministic or Nondeterministic Emerson-Lei Automata. Online. In Yu-Fang Chen, Chih-Hong Cheng, Javier Esparza. \textit{Automated Technology for Verification and Analysis - 17th International Symposium, ATVA 2019, Taipei, Taiwan, October 28-31, 2019, Proceedings}. Cham (Switzerland): Springer, 2019, s.~357-365. ISBN~978-3-030-31783-6. Dostupné z: https://dx.doi.org/10.1007/978-3-030-31784-3\_{}21.

Podrobný výpis o publikaci