Tighter Construction of Tight Büchi Automata

Result code in 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>

Result on the web

<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>

Result language

angličtina

Original language name

Tighter Construction of Tight Büchi Automata

Original language description

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.

Czech name

—

Czech description

—

Type

D - Article in proceedings

CEP classification

—

OECD FORD branch

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

Project

<a href="/en/project/GA23-06506S" target="_blank" >GA23-06506S: Advanced Analysis and Verification for Advanced Software</a><br>

Continuities

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

Publication year

2024

Confidentiality

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

Article name in the collection

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

Number of pages

22

Pages from-to

234-255

Publisher name

Springer

Place of publication

Cham

Event location

Luxembourg City, Luxembourg

Event date

Jan 1, 2024

Type of event by nationality

WRD - Celosvětová akce

UT code for WoS article

001284197300012