Mechanizing the Minimization of Deterministic Generalized Büchi Automata

Abstract : Deterministic Büchi automata (DBA) are useful to (probabilistic) model checking and synthesis. We survey techniques used to obtain and minimize DBAs for different classes of properties. We extend these techniques to support DBA that have generalized and transition-based acceptance (DTGBA) as they can be even smaller. Our minimization technique - a reduction to a SAT problem - synthesizes a DTGBA equivalent to the input DTGBA for any given number of states and number of acceptance sets (assuming such automaton exists). We present benchmarks using a framework that implements all these techniques.
Document type :
Conference papers
Complete list of metadatas

Cited literature [22 references]  Display  Hide  Download

https://hal.archives-ouvertes.fr/hal-01215522
Contributor : Lip6 Publications <>
Submitted on : Tuesday, November 22, 2016 - 10:06:28 AM
Last modification on : Thursday, March 21, 2019 - 1:20:58 PM
Long-term archiving on : Tuesday, March 21, 2017 - 10:26:03 AM

File

978-3-662-43613-4_17_Chapter.p...
Files produced by the author(s)

Licence


Distributed under a Creative Commons Attribution 4.0 International License

Identifiers

Citation

Souheib Baarir, Alexandre Duret-Lutz. Mechanizing the Minimization of Deterministic Generalized Büchi Automata. 34th Formal Techniques for Networked and Distributed Systems (FORTE), Jun 2014, Berlin, Germany. pp.266-283, ⟨10.1007/978-3-662-43613-4_17⟩. ⟨hal-01215522⟩

Share

Metrics

Record views

239

Files downloads

92