D
2023
Reducing Acceptance Marks in Emerson-Lei Automata by QBF Solving
SCHWARZOVÁ, Tereza, Jan STREJČEK a Juraj MAJOR
Základní údaje
Originální název
Reducing Acceptance Marks in Emerson-Lei Automata by QBF Solving
Autoři
SCHWARZOVÁ, Tereza (203 Česká republika, domácí),
Jan STREJČEK (203 Česká republika, garant, domácí) a
Juraj MAJOR (703 Slovensko, domácí)
Vydání
Dagstuhl, Germany, 26th International Conference on Theory and Applications of Satisfiability Testing, SAT 2023, July 4-8, 2023, Alghero, Italy, od s. 1-20, 20 s. 2023
Nakladatel
Schloss Dagstuhl - Leibniz-Zentrum für Informatik
Další údaje
Typ výsledku
Stať ve sborníku
Obor
10201 Computer sciences, information science, bioinformatics
Utajení
není předmětem státního či obchodního tajemství
Forma vydání
elektronická verze "online"
Kód RIV
RIV/00216224:14330/23:00131935
Organizační jednotka
Fakulta informatiky
Klíčová slova anglicky
Emerson-Lei automata; TELA; automata reduction; QBF; telatko
Příznaky
Mezinárodní význam, Recenzováno
V originále
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ávaznosti
MUNI/A/1433/2022, interní kód MU | Název: Zapojení studentů Fakulty informatiky do mezinárodní vědecké komunity 23 | Investor: Masarykova univerzita, Zapojení studentů Fakulty informatiky do mezinárodní vědecké komunity 23 |
|
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 |
|
Zobrazeno: 4. 11. 2024 16:12