%0 Conference Proceedings
%T Mechanizing the Minimization of Deterministic Generalized Büchi Automata
%+ Université Paris Nanterre (UPN)
%+ Modélisation et Vérification (MoVe)
%+ Laboratoire de Recherche et de Développement de l'EPITA (LRDE)
%A Baarir, Souheib
%A Duret-Lutz, Alexandre
%Z Part 4: Bisimulation, Abstraction and Reduction
%< avec comité de lecture
%( Formal Techniques for Distributed Objects, Components, and Systems
%B 34th Formal Techniques for Networked and Distributed Systems (FORTE)
%C Berlin, Germany
%Y Erika Ábrahám
%Y Catuscia Palamidessi
%I Springer
%3 Lecture Notes in Computer Science
%V 8461
%P 266-283
%8 2014-06-03
%D 2014
%R 10.1007/978-3-662-43613-4_17
%Z Computer Science [cs]Conference papers
%X 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.
%G English
%Z TC 6
%Z WG 6.1
%2 https://hal.science/hal-01215522/document
%2 https://hal.science/hal-01215522/file/978-3-662-43613-4_17_Chapter.pdf
%L hal-01215522
%U https://hal.science/hal-01215522
%~ UPMC
%~ CNRS
%~ UNIV-PARIS10
%~ LIP6
%~ IFIP-LNCS
%~ IFIP
%~ IFIP-TC
%~ IFIP-WG
%~ IFIP-TC6
%~ IFIP-WG6-1
%~ IFIP-FORTE
%~ IFIP-LNCS-8461
%~ UPMC_POLE_1
%~ SORBONNE-UNIVERSITE
%~ SU-SCIENCES
%~ UNIV-PARIS-LUMIERES
%~ SU-TI
%~ UNIV-PARIS-NANTERRE
%~ ALLIANCE-SU