Reducing Acceptance Marks in Emerson-Lei Automata by QBF Solving

Kód výsledku v IS VaVaI

<a href="https://www.isvavai.cz/riv?ss=detail&h=RIV%2F00216224%3A14330%2F23%3A00131935" target="_blank" >RIV/00216224:14330/23:00131935 - isvavai.cz</a>

Výsledek na webu

<a href="https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.SAT.2023.23" target="_blank" >https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.SAT.2023.23</a>

DOI - Digital Object Identifier

<a href="http://dx.doi.org/10.4230/LIPIcs.SAT.2023.23" target="_blank" >10.4230/LIPIcs.SAT.2023.23</a>

Jazyk výsledku

angličtina

Název v původním jazyce

Reducing Acceptance Marks in Emerson-Lei Automata by QBF Solving

Popis výsledku v původním jazyce

This paper presents a novel application of QBF solving to automata reduction. We focus on Transition-based Emerson-Lei automata (TELA), which is a popular formalism that generalizes many traditional kinds of automata over infinite words including Büchi, co-Büchi, Rabin, Streett, and parity automata. Transitions in a TELA are labelled with acceptance marks and its accepting formula is a positive Boolean combination of atoms saying that a particular mark has to be visited infinitely or finitely often. Algorithms processing these automata are often very sensitive to the number of acceptance marks. We introduce a new technique for reducing the number of acceptance marks in TELA based on satisfiability of quantified Boolean formulas (QBF). We evaluated our reduction technique on TELA produced by state-of-the-art tools of the libraries Owl and Spot and by the tool ltl3tela. The technique reduced some acceptance marks in automata produced by all the tools. On automata with more than one acceptance mark obtained by translation of LTL formulas from literature with tools Delag and Rabinizer 4, our technique reduced 27.7% and 39.3% of acceptance marks, respectively. The reduction was even higher on automata from random formulas.

Název v anglickém jazyce

Reducing Acceptance Marks in Emerson-Lei Automata by QBF Solving

Popis výsledku anglicky

This paper presents a novel application of QBF solving to automata reduction. We focus on Transition-based Emerson-Lei automata (TELA), which is a popular formalism that generalizes many traditional kinds of automata over infinite words including Büchi, co-Büchi, Rabin, Streett, and parity automata. Transitions in a TELA are labelled with acceptance marks and its accepting formula is a positive Boolean combination of atoms saying that a particular mark has to be visited infinitely or finitely often. Algorithms processing these automata are often very sensitive to the number of acceptance marks. We introduce a new technique for reducing the number of acceptance marks in TELA based on satisfiability of quantified Boolean formulas (QBF). We evaluated our reduction technique on TELA produced by state-of-the-art tools of the libraries Owl and Spot and by the tool ltl3tela. The technique reduced some acceptance marks in automata produced by all the tools. On automata with more than one acceptance mark obtained by translation of LTL formulas from literature with tools Delag and Rabinizer 4, our technique reduced 27.7% and 39.3% of acceptance marks, respectively. The reduction was even higher on automata from random formulas.

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

—

Návaznosti

S - Specificky vyzkum na vysokych skolach<br>I - Institucionalni podpora na dlouhodoby koncepcni rozvoj vyzkumne organizace

Rok uplatnění

2023

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

26th International Conference on Theory and Applications of Satisfiability Testing, SAT 2023, July 4-8, 2023, Alghero, Italy

ISBN

9783959772860

ISSN

1868-8969

e-ISSN

—

Počet stran výsledku

20

Strana od-do

1-20

Název nakladatele

Schloss Dagstuhl - Leibniz-Zentrum für Informatik

Místo vydání

Dagstuhl, Germany

Místo konání akce

Alghero, Italy

Datum konání akce

1. 1. 2023

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

WRD - Celosvětová akce

Kód UT WoS článku

—