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.
This work has been supported by the project ImpRo/ANR-2010-BLAN-0317.
Chapter PDF
Similar content being viewed by others
Keywords
- Model Check
- Generalize Acceptance
- Acceptance Condition
- Strongly Connect Component
- Deterministic Generalize
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.
References
Audemard, G., Simon, L.: Predicting learnt clauses quality in modern SAT solvers. In: IJCAI 2009, pp. 399–404 (July 2009)
Babiak, T., Badie, T., Duret-Lutz, A., Křetínský, M., Strejček, J.: Compositional approach to suspension and other improvements to LTL translation. In: Bartocci, E., Ramakrishnan, C.R. (eds.) SPIN 2013. LNCS, vol. 7976, pp. 81–98. Springer, Heidelberg (2013)
Baier, C., Katoen, J.-P.: Principles of Model Checking. MIT Press (2008)
Bloem, R., Ravi, K., Somenzi, F.: Efficient decision procedures for model checking of linear time logic properties. In: Halbwachs, N., Peled, D.A. (eds.) CAV 1999. LNCS, vol. 1633, pp. 222–235. Springer, Heidelberg (1999)
Boigelot, B., Jodogne, S., Wolper, P.: On the use of weak automata for deciding linear arithmetic with integer and real variables. In: Goré, R.P., Leitsch, A., Nipkow, T. (eds.) IJCAR 2001. LNCS (LNAI), vol. 2083, pp. 611–625. Springer, Heidelberg (2001)
Černá, I., Pelánek, R.: Relating hierarchy of temporal properties to model checking. In: Rovan, B., Vojtáš, P. (eds.) MFCS 2003. LNCS, vol. 2747, pp. 318–327. Springer, Heidelberg (2003)
Clemente, L., Mayr, R.: Advanced automata minimization. In: POPL 2013, pp. 63–74. ACM (2013)
Couvreur, J.-M., Duret-Lutz, A., Poitrenaud, D.: On-the-fly emptiness checks for generalized büchi automata. In: Godefroid, P. (ed.) SPIN 2005. LNCS, vol. 3639, pp. 169–184. Springer, Heidelberg (2005)
Dax, C., Eisinger, J., Klaedtke, F.: Mechanizing the powerset construction for restricted classes of ω-automata. In: Namjoshi, K.S., Yoneda, T., Higashino, T., Okamura, Y. (eds.) ATVA 2007. LNCS, vol. 4762, pp. 223–236. Springer, Heidelberg (2007)
Duret-Lutz, A.: LTL translation improvements in Spot. In: VECoS 2011. British Computer Society (September 2011)
Ehlers, R.: Minimising deterministic büchi automata precisely using SAT solving. In: Strichman, O., Szeider, S. (eds.) SAT 2010. LNCS, vol. 6175, pp. 326–332. Springer, Heidelberg (2010)
Gaiser, A., Křetínský, J., Esparza, J.: Rabinizer: Small deterministic automata for lTL(F,G). In: Chakraborty, S., Mukund, M. (eds.) ATVA 2012. LNCS, vol. 7561, pp. 72–76. Springer, Heidelberg (2012)
Finkbeiner, B., Schewe, S.: Uniform distributed synthesis. In: LICS 2005, pp. 321–330 (June 2005)
Klein, J., Baier, C.: Experiments with deterministic ω-automata for formulas of linear temporal logic. Theoretical Computer Science 363, 182–195 (2005)
Krishnan, S.C., Puri, A., Brayton, R.K.: Deterministic ω-automata vis-a-vis deterministic Büchi automata. In: Du, D.-Z., Zhang, X.-S. (eds.) ISAAC 1994. LNCS, vol. 834, pp. 378–386. Springer, Heidelberg (1994)
Löding, C.: Efficient minimization of deterministic weak ω-automata. Information Processing Letters 79(3), 105–109 (2001)
Maler, O., Staiger, L.: On syntactic congruences for ω-languages. In: Enjalbert, P., Wagner, K.W., Finkel, A. (eds.) STACS 1993. LNCS, vol. 665, pp. 586–594. Springer, Heidelberg (1993)
Manna, Z., Pnueli, A.: A hierarchy of temporal properties. In: PODC 1990, pp. 377–410. ACM (1990)
Rozier, K.Y., Vardi, M.Y.: A multi-encoding approach for LTL symbolic satisfiability checking. In: Butler, M., Schulte, W. (eds.) FM 2011. LNCS, vol. 6664, pp. 417–431. Springer, Heidelberg (2011)
Safra, S.: Complexity of Automata on Infinite Objects. PhD thesis, The Weizmann Institute of Science, Rehovot, Israel (March 1989)
Schewe, S.: Beyond hyper-minimisation—minimising DBAs and DPAs is NP-complete. In: FSTTCS 2010. LIPIcs, vol. 8, pp. 400–411. Schloss Dagstuhl LZI (2010)
Schewe, S., Varghese, T.: Tight bounds for the determinisation and complementation of generalised büchi automata. In: Chakraborty, S., Mukund, M. (eds.) ATVA 2012. LNCS, vol. 7561, pp. 42–56. Springer, Heidelberg (2012)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2014 IFIP International Federation for Information Processing
About this paper
Cite this paper
Baarir, S., Duret-Lutz, A. (2014). Mechanizing the Minimization of Deterministic Generalized Büchi Automata. In: Ábrahám, E., Palamidessi, C. (eds) Formal Techniques for Distributed Objects, Components, and Systems. FORTE 2014. Lecture Notes in Computer Science, vol 8461. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-662-43613-4_17
Download citation
DOI: https://doi.org/10.1007/978-3-662-43613-4_17
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-662-43612-7
Online ISBN: 978-3-662-43613-4
eBook Packages: Computer ScienceComputer Science (R0)