Tighter Construction of Tight Büchi Automata

D 2024

Tighter Construction of Tight Büchi Automata

JANKOLA, Marek a Jan STREJČEK

Základní údaje

Originální název

Tighter Construction of Tight Büchi Automata

Autoři

JANKOLA, Marek a Jan STREJČEK

Vydání

Cham, Foundations of Software Science and Computation Structures - 27th International Conference, FoSSaCS 2024, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2024, Luxembourg City, Luxembourg, April 6-11, 2024, Proceedings, Part I, od s. 234-255, 22 s. 2024

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í

elektronická verze "online"

Odkazy

URL

Impakt faktor

Impact factor: 0.402 v roce 2005

Kód RIV

RIV/00216224:14330/24:00135862

Organizační jednotka

Fakulta informatiky

ISBN

978-3-031-57227-2

ISSN

DOI

https://doi.org/10.1007/978-3-031-57228-9_12

UT WoS

001284197300012

EID Scopus

2-s2.0-85192207746

Klíčová slova anglicky

tight automata; shortest counterexamples; LTL

Štítky

core_A, firank_A, formela-aut, formela-conference, linear temporal logic, LTL, omega-automata, verification, 𝜔-automata

Příznaky

Mezinárodní význam, Recenzováno

Změněno: 10. 7. 2025 18:04, prof. RNDr. Jan Strejček, Ph.D.

Anotace

V originále

Tight automata are useful in providing the shortest counterexample in LTL model checking and also in constructing a maximally satisfying strategy in LTL strategy synthesis. There exists a translation of LTL formulas to tight Büchi automata and several translations of Büchi automata to equivalent tight Büchi automata. This paper presents another translation of Büchi automata to equivalent tight Büchi automata. The translation is designed to produce smaller tight automata and it asymptotically improves the best-known upper bound on the size of a tight Büchi automaton equivalent to a given Büchi automaton. We also provide a lower bound, which is more precise than the previously known one. Further, we show that automata reduction methods based on quotienting preserve tightness. Our translation was implemented in a tool called Tightener. Experimental evaluation shows that Tightener usually produces smaller tight automata than the translation from LTL to tight automata known as CGH.

Návaznosti

GA23-06506S, projekt VaV

Název: Pokročilá analýza a verifikace pro pokročilý software

Investor: Grantová agentura ČR, Pokročilá analýza a verifikace pro pokročilý software

101087529, interní kód MU

Název: Cyber-security Excellence Hub in Estonia and South Moravia (CHESS)

Investor: Evropská unie, Cyber-security Excellence Hub in Estonia and South Moravia (CHESS), Rozšiřování účasti a posílení ERA

Citovat

JANKOLA, Marek a Jan STREJČEK. Tighter Construction of Tight Büchi Automata. Online. In Naoki Kobayashi and James Worrell. Foundations of Software Science and Computation Structures - 27th International Conference, FoSSaCS 2024, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2024, Luxembourg City, Luxembourg, April 6-11, 2024, Proceedings, Part I. Cham: Springer, 2024, s. 234-255. ISBN 978-3-031-57227-2. Dostupné z: https://doi.org/10.1007/978-3-031-57228-9_12.

@inproceedings{2396421,
   author = {Jankola, Marek and Strejček, Jan},
   address = {Cham},
   booktitle = {Foundations of Software Science and Computation Structures - 27th International Conference, FoSSaCS 2024, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2024, Luxembourg City, Luxembourg, April 6-11, 2024, Proceedings, Part I},
   doi = {https://doi.org/10.1007/978-3-031-57228-9_12},
   editor = {Naoki Kobayashi and James Worrell},
   keywords = {tight automata; shortest counterexamples; LTL},
   howpublished = {elektronická verze "online"},
   language = {eng},
   location = {Cham},
   isbn = {978-3-031-57227-2},
   pages = {234-255},
   publisher = {Springer},
   title = {Tighter Construction of Tight Büchi Automata},
   url = {https://link.springer.com/chapter/10.1007/978-3-031-57228-9_12},
   year = {2024}
}

TY  - CONF
ID  - 2396421
AU  - Jankola, Marek - Strejček, Jan
PY  - 2024
TI  - Tighter Construction of Tight Büchi Automata
PB  - Springer
CY  - Cham
SN  - 9783031572272
KW  - tight automata
KW  - shortest counterexamples
KW  - LTL
UR  - https://link.springer.com/chapter/10.1007/978-3-031-57228-9_12
N2  - Tight automata are useful in providing the shortest counterexample in LTL model checking and also in constructing a maximally satisfying strategy in LTL strategy synthesis. There exists a translation of LTL formulas to tight Büchi automata and several translations of Büchi automata to equivalent tight Büchi automata. This paper presents another translation of Büchi automata to equivalent tight Büchi automata. The translation is designed to produce smaller tight automata and it asymptotically improves the best-known upper bound on the size of a tight Büchi automaton equivalent to a given Büchi automaton. We also provide a lower bound, which is more precise than the previously known one. Further, we show that automata reduction methods based on quotienting preserve tightness. Our translation was implemented in a tool called Tightener. Experimental evaluation shows that Tightener usually produces smaller tight automata than the translation from LTL to tight automata known as CGH.
ER  -

JANKOLA, Marek a Jan STREJČEK. Tighter Construction of Tight Büchi Automata. Online. In Naoki Kobayashi and James Worrell. \textit{Foundations of Software Science and Computation Structures - 27th International Conference, FoSSaCS 2024, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2024, Luxembourg City, Luxembourg, April 6-11, 2024, Proceedings, Part I}. Cham: Springer, 2024, s.~234-255. ISBN~978-3-031-57227-2. Dostupné z: https://doi.org/10.1007/978-3-031-57228-9\_{}12.

Přehled o publikaci