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
Zobrazeno: 11. 11. 2024 07:48