Tighter Construction of Tight Büchi Automata

Kód výsledku v IS VaVaI

<a href="https://www.isvavai.cz/riv?ss=detail&h=RIV%2F00216224%3A14330%2F24%3A00135862" target="_blank" >RIV/00216224:14330/24:00135862 - isvavai.cz</a>

Výsledek na webu

<a href="https://link.springer.com/chapter/10.1007/978-3-031-57228-9_12" target="_blank" >https://link.springer.com/chapter/10.1007/978-3-031-57228-9_12</a>

DOI - Digital Object Identifier

<a href="http://dx.doi.org/10.1007/978-3-031-57228-9_12" target="_blank" >10.1007/978-3-031-57228-9_12</a>

Jazyk výsledku

angličtina

Název v původním jazyce

Tighter Construction of Tight Büchi Automata

Popis výsledku v původním jazyce

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ázev v anglickém jazyce

Tighter Construction of Tight Büchi Automata

Popis výsledku anglicky

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.

Druh

D - Stať ve sborníku

CEP obor

—

OECD FORD obor

10201 - Computer sciences, information science, bioinformathics (hardware development to be 2.2, social aspect to be 5.8)

Projekt

<a href="/cs/project/GA23-06506S" target="_blank" >GA23-06506S: Pokročilá analýza a verifikace pro pokročilý software</a><br>

Návaznosti

P - Projekt vyzkumu a vyvoje financovany z verejnych zdroju (s odkazem do CEP)<br>S - Specificky vyzkum na vysokych skolach<br>I - Institucionalni podpora na dlouhodoby koncepcni rozvoj vyzkumne organizace

Rok uplatnění

2024

Kód důvěrnosti údajů

S - Úplné a pravdivé údaje o projektu nepodléhají ochraně podle zvláštních právních předpisů

Název statě ve sborníku

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

ISBN

9783031572272

ISSN

0302-9743

e-ISSN

1611-3349

Počet stran výsledku

22

Strana od-do

234-255

Název nakladatele

Springer

Místo vydání

Cham

Místo konání akce

Luxembourg City, Luxembourg

Datum konání akce

1. 1. 2024

Typ akce podle státní příslušnosti

WRD - Celosvětová akce

Kód UT WoS článku

001284197300012