Reducing Acceptance Marks in Emerson-Lei Automata by QBF
Solving

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

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

Kód RIV

RIV/00216224:14330/23:00131935

Organizační jednotka

Fakulta informatiky

ISBN

978-3-95977-286-0

ISSN

DOI

http://dx.doi.org/10.4230/LIPIcs.SAT.2023.23

Klíčová slova anglicky

Emerson-Lei automata; TELA; automata reduction; QBF; telatko

Štítky

core_A, firank_A, formela-aut, formela-conference, omega-automata, satisfiability, 𝜔-automata

Příznaky

Mezinárodní význam, Recenzováno

Změněno: 19. 3. 2024 13:57, prof. RNDr. Jan Strejček, Ph.D.

Anotace

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

Citovat

SCHWARZOVÁ, Tereza, Jan STREJČEK a Juraj MAJOR. Reducing Acceptance Marks in Emerson-Lei Automata by QBF Solving. Online. In Meena Mahajan and Friedrich Slivovsky. 26th International Conference on Theory and Applications of Satisfiability Testing, SAT 2023, July 4-8, 2023, Alghero, Italy. Dagstuhl, Germany: Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2023, s. 1-20. ISBN 978-3-95977-286-0. Dostupné z: https://dx.doi.org/10.4230/LIPIcs.SAT.2023.23.

@inproceedings{2326760,
   author = {Schwarzová, Tereza and Strejček, Jan and Major, Juraj},
   address = {Dagstuhl, Germany},
   booktitle = {26th International Conference on Theory and Applications of Satisfiability Testing, SAT 2023, July 4-8, 2023, Alghero, Italy},
   doi = {http://dx.doi.org/10.4230/LIPIcs.SAT.2023.23},
   editor = {Meena Mahajan and Friedrich Slivovsky},
   keywords = {Emerson-Lei automata; TELA; automata reduction; QBF; telatko},
   howpublished = {elektronická verze "online"},
   language = {eng},
   location = {Dagstuhl, Germany},
   isbn = {978-3-95977-286-0},
   pages = {1-20},
   publisher = {Schloss Dagstuhl - Leibniz-Zentrum für Informatik},
   title = {Reducing Acceptance Marks in Emerson-Lei Automata by QBF Solving},
   url = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.SAT.2023.23},
   year = {2023}
}

TY  - JOUR
ID  - 2326760
AU  - Schwarzová, Tereza - Strejček, Jan - Major, Juraj
PY  - 2023
TI  - Reducing Acceptance Marks in Emerson-Lei Automata by QBF Solving
PB  - Schloss Dagstuhl - Leibniz-Zentrum für Informatik
CY  - Dagstuhl, Germany
SN  - 9783959772860
KW  - Emerson-Lei automata
KW  - TELA
KW  - automata reduction
KW  - QBF
KW  - telatko
UR  - https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.SAT.2023.23
N2  - 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.
ER  -

SCHWARZOVÁ, Tereza, Jan STREJČEK a Juraj MAJOR. Reducing Acceptance Marks in Emerson-Lei Automata by QBF Solving. Online. In Meena Mahajan and Friedrich Slivovsky. \textit{26th International Conference on Theory and Applications of Satisfiability Testing, SAT 2023, July 4-8, 2023, Alghero, Italy}. Dagstuhl, Germany: Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2023, s.~1-20. ISBN~978-3-95977-286-0. Dostupné z: https://dx.doi.org/10.4230/LIPIcs.SAT.2023.23.

Podrobný výpis o publikaci