DROPS

Document

DOI: 10.4230/LIPIcs.SAT.2023.23

Reducing Acceptance Marks in Emerson-Lei Automata by QBF Solving

Authors: Tereza Schwarzová, Jan Strejček, and Juraj Major

Published in: LIPIcs, Volume 271, 26th International Conference on Theory and Applications of Satisfiability Testing (SAT 2023)

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.

Cite as

Tereza Schwarzová, Jan Strejček, and Juraj Major. Reducing Acceptance Marks in Emerson-Lei Automata by QBF Solving. In 26th International Conference on Theory and Applications of Satisfiability Testing (SAT 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 271, pp. 23:1-23:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)

Copy BibTex To Clipboard

@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/entities/document/10.4230/LIPIcs.SAT.2023.23},
  URN =		{urn:nbn:de:0030-drops-184859},
  doi =		{10.4230/LIPIcs.SAT.2023.23},
  annote =	{Keywords: Emerson-Lei automata, TELA, automata reduction, QBF, telatko}
}

Document

DOI: 10.4230/DagSemProc.06081.6

Reachability analysis of multithreaded software with asynchronous communication

Authors: Ahmed Bouajjani, Javier Esparza, Stefan Schwoon, and Jan Strejcek

Published in: Dagstuhl Seminar Proceedings, Volume 6081, Software Verification: Infinite-State Model Checking and Static Program Analysis (2006)

Abstract

We introduce asynchronous dynamic pushdown networks (ADPN), a new model for multithreaded programs in which pushdown systems communicate via shared memory. ADPN generalizes both CPS (concurrent pushdown systems) and DPN (dynamic pushdown networks). We show that ADPN exhibit several advantages as a program model. Since the reachability problem for ADPN is undecidable even in the case without dynamic creation of processes, we address the bounded reachability problem, which considers only those computation sequences where the (index of the) thread accessing the shared memory is changed at most a fixed given number of times. We provide efficient algorithms for both forward and backward reachability analysis. The algorithms are based on automata techniques for symbolic representation of sets of configurations. This talk is based on joint work with Ahmed Bouajjani, Javier Esparza, and Jan Strejcek that appeared in FSTTCS 2005.

Cite as

Ahmed Bouajjani, Javier Esparza, Stefan Schwoon, and Jan Strejcek. Reachability analysis of multithreaded software with asynchronous communication. In Software Verification: Infinite-State Model Checking and Static Program Analysis. Dagstuhl Seminar Proceedings, Volume 6081, pp. 1-18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2006)

Copy BibTex To Clipboard

@InProceedings{bouajjani_et_al:DagSemProc.06081.6,
  author =	{Bouajjani, Ahmed and Esparza, Javier and Schwoon, Stefan and Strejcek, Jan},
  title =	{{Reachability analysis of multithreaded software with asynchronous communication}},
  booktitle =	{Software Verification: Infinite-State Model Checking and Static Program Analysis},
  pages =	{1--18},
  series =	{Dagstuhl Seminar Proceedings (DagSemProc)},
  ISSN =	{1862-4405},
  year =	{2006},
  volume =	{6081},
  editor =	{Parosh Aziz Abdulla and Ahmed Bouajjani and Markus M\"{u}ller-Olm},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/DagSemProc.06081.6},
  URN =		{urn:nbn:de:0030-drops-7263},
  doi =		{10.4230/DagSemProc.06081.6},
  annote =	{Keywords: Model checking, pushdown systems, concurrency}
}

Search Results

Documents authored by Strejcek, Jan

Reducing Acceptance Marks in Emerson-Lei Automata by QBF Solving

Abstract

Cite as

Reachability analysis of multithreaded software with asynchronous communication

Abstract

Cite as

Thanks for your feedback!

Could not send message