SCHWARZOVÁ, Tereza, Jan STREJČEK and 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, p. 1-20. ISBN 978-3-95977-286-0. Available from: https://dx.doi.org/10.4230/LIPIcs.SAT.2023.23.
Other formats:   BibTeX LaTeX RIS
Basic information
Original name Reducing Acceptance Marks in Emerson-Lei Automata by QBF Solving
Authors SCHWARZOVÁ, Tereza (203 Czech Republic, belonging to the institution), Jan STREJČEK (203 Czech Republic, guarantor, belonging to the institution) and Juraj MAJOR (703 Slovakia, belonging to the institution).
Edition Dagstuhl, Germany, 26th International Conference on Theory and Applications of Satisfiability Testing, SAT 2023, July 4-8, 2023, Alghero, Italy, p. 1-20, 20 pp. 2023.
Publisher Schloss Dagstuhl - Leibniz-Zentrum für Informatik
Other information
Original language English
Type of outcome Proceedings paper
Field of Study 10201 Computer sciences, information science, bioinformatics
Country of publisher Germany
Confidentiality degree is not subject to a state or trade secret
Publication form electronic version available online
WWW URL
RIV identification code RIV/00216224:14330/23:00131935
Organization unit Faculty of Informatics
ISBN 978-3-95977-286-0
ISSN 1868-8969
Doi http://dx.doi.org/10.4230/LIPIcs.SAT.2023.23
Keywords in English Emerson-Lei automata; TELA; automata reduction; QBF; telatko
Tags formela-aut, formela-conference, omega-automata, satisfiability, 𝜔-automata
Tags International impact, Reviewed
Changed by Changed by: prof. RNDr. Jan Strejček, Ph.D., učo 3366. Changed: 19/3/2024 13:57.
Abstract
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.
Links
MUNI/A/1433/2022, interní kód MUName: Zapojení studentů Fakulty informatiky do mezinárodní vědecké komunity 23
Investor: Masaryk University
101087529, interní kód MUName: Cyber-security Excellence Hub in Estonia and South Moravia (CHESS)
Investor: European Union, Cyber-security Excellence Hub in Estonia and South Moravia (CHESS), Widening participation and strengthening the European Research Area
PrintDisplayed: 8/6/2024 11:02