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.

Basic information

Original name

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

Authors

MAJOR, Juraj (703 Slovakia, belonging to the institution), František BLAHOUDEK (203 Czech Republic), Jan STREJČEK (203 Czech Republic, guarantor, belonging to the institution), Miriama JÁNOŠOVÁ (703 Slovakia, belonging to the institution) and Tatiana ZBONČÁKOVÁ (703 Slovakia, belonging to the institution)

Edition

Cham (Switzerland), Automated Technology for Verification and Analysis - 17th International Symposium, ATVA 2019, Taipei, Taiwan, October 28-31, 2019, Proceedings, p. 357-365, 9 pp. 2019

Publisher

Springer

Other information

Language

English

Type of outcome

Stať ve sborníku

Field of Study

10200 1.2 Computer and information sciences

Country of publisher

Switzerland

Confidentiality degree

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

Publication form

electronic version available online

References:

URL

Impact factor

Impact factor: 0.402 in 2005

RIV identification code

RIV/00216224:14330/19:00107770

Organization unit

Faculty of Informatics

ISBN

978-3-030-31783-6

ISSN

DOI

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

UT WoS

000723515700021

Keywords in English

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

Abstract

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.

Links

GA19-24397S, research and development project

Name: Automaty v rozhodovacích procedurách a verifikaci (Acronym: AUTODEV)

Investor: Czech Science Foundation

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

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

Investor: Masaryk University, Category A

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

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

Investor: Masaryk University, Category A

Citovat

MAJOR, Juraj, František BLAHOUDEK, Jan STREJČEK, Miriama JÁNOŠOVÁ and 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, p. 357-365. ISBN 978-3-030-31783-6. Available from: 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Á and 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, p.~357-365. ISBN~978-3-030-31783-6. Available from: https://dx.doi.org/10.1007/978-3-030-31784-3\_{}21.

Detailed Information on Publication Record