License: Creative Commons Attribution 4.0 International license (CC BY 4.0)
When quoting this document, please refer to the following
DOI: 10.4230/LIPIcs.SAT.2023.23
URN: urn:nbn:de:0030-drops-184859
URL: http://dagstuhl.sunsite.rwth-aachen.de/volltexte/2023/18485/
Go to the corresponding LIPIcs Volume Portal


Schwarzová, Tereza ; Strejček, Jan ; Major, Juraj

Reducing Acceptance Marks in Emerson-Lei Automata by QBF Solving

pdf-format:
LIPIcs-SAT-2023-23.pdf (0.9 MB)


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.

BibTeX - Entry

@InProceedings{schwarzova_et_al:LIPIcs.SAT.2023.23,
  author =	{Schwarzov\'{a}, Tereza and Strej\v{c}ek, Jan and Major, Juraj},
  title =	{{Reducing Acceptance Marks in Emerson-Lei Automata by QBF Solving}},
  booktitle =	{26th International Conference on Theory and Applications of Satisfiability Testing (SAT 2023)},
  pages =	{23:1--23:20},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-286-0},
  ISSN =	{1868-8969},
  year =	{2023},
  volume =	{271},
  editor =	{Mahajan, Meena and Slivovsky, Friedrich},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/opus/volltexte/2023/18485},
  URN =		{urn:nbn:de:0030-drops-184859},
  doi =		{10.4230/LIPIcs.SAT.2023.23},
  annote =	{Keywords: Emerson-Lei automata, TELA, automata reduction, QBF, telatko}
}

Keywords: Emerson-Lei automata, TELA, automata reduction, QBF, telatko
Collection: 26th International Conference on Theory and Applications of Satisfiability Testing (SAT 2023)
Issue Date: 2023
Date of publication: 09.08.2023
Supplementary Material: Software: https://gitlab.fi.muni.cz/xschwar3/telatko archived at: https://archive.softwareheritage.org/swh:1:dir:ce6c69759d7317f0bc9cb2dc2cc96e9473ca31cd


DROPS-Home | Fulltext Search | Imprint | Privacy Published by LZI