Skip to main content
SpringerLink
Log in
Book cover

International Conference on Theory and Applications of Satisfiability Testing

SAT 2010: Theory and Applications of Satisfiability Testing – SAT 2010 pp 326–332Cite as

Minimising Deterministic Büchi Automata Precisely Using SAT Solving

  • Conference paper

Part of the book series: Lecture Notes in Computer Science ((LNTCS,volume 6175))

Abstract

We show how deterministic Büchi automata can be fully minimised by reduction to the satisfiability (SAT) problem, yielding the first automated method for this task. Size reduction of such ω-automata is an important step in probabilistic model checking as well as synthesis of finite-state systems. Our experiments demonstrate that state-of-the-art SAT solvers are capable of solving the resulting satisfiability problem instances quickly, making the approach presented valuable in practice.

This work was supported by the German Research Foundation (DFG) within the program “Performance Guarantees for Computer Systems” and the Transregional Collaborative Research Center “Automatic Verification and Analysis of Complex Systems” (SFB/TR 14 AVACS).

This is a preview of subscription content, log in via an institution.

Chapter
USD   29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD   39.99
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD   54.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Learn about institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. Baier, C., Katoen, J.P.: Principles of Model Checking. MIT Press, Cambridge (2008)

    MATH  Google Scholar 

  2. Barrett, C., Sebastiani, R., Seshia, S., Tinelli, C.: Satisfiability Modulo Theories. In: [5], pp. 825–885.

    Google Scholar 

  3. Biere, A.: Picosat essentials. JSAT 4(2-4), 75–97 (2008)

    MATH  Google Scholar 

  4. Biere, A.: Bounded Model Checking. In: [5], pp. 457–474

    Google Scholar 

  5. Biere, A., Heule, M., van Maaren, H., Walsh, T. (eds.): Handbook of Satisfiability. IOS Press, Amsterdam (2009)

    MATH  Google Scholar 

  6. Bloem, R., Galler, S., Jobstmann, B., Piterman, N., Pnueli, A., Weiglhofer, M.: Specify, compile, run: Hardware from PSL. Electr. Notes Theor. Comput. Sci. 190(4), 3–16 (2007)

    Article  Google Scholar 

  7. Etessami, K., Holzmann, G.J.: Optimizing Büchi automata. In: Palamidessi, C. (ed.) CONCUR 2000. LNCS, vol. 1877, pp. 153–167. Springer, Heidelberg (2000)

    Chapter  Google Scholar 

  8. Etessami, K., Wilke, T., Schuller, R.A.: Fair simulation relations, parity games, and state space reduction for Büchi automata. SIAM J. Comput. 34(5), 1159–1175 (2005)

    Article  MathSciNet  MATH  Google Scholar 

  9. Gastin, P., Oddoux, D.: Fast LTL to Büchi automata translation. In: Berry, G., Comon, H., Finkel, A. (eds.) CAV 2001. LNCS, vol. 2102, pp. 53–65. Springer, Heidelberg (2001)

    Chapter  Google Scholar 

  10. Klein, J., Baier, C.: Experiments with deterministic ω-automata for formulas of linear temporal logic. Theor. Comput. Sci. 363(2), 182–195 (2006)

    Article  MathSciNet  MATH  Google Scholar 

  11. Krishnan, S.C., Puri, A., Brayton, R.K.: Deterministic w automata vis-a-vis deterministic buchi automata. In: Du, D.-Z., Zhang, X.-S. (eds.) ISAAC 1994. LNCS, vol. 834, pp. 378–386. Springer, Heidelberg (1994)

    Chapter  Google Scholar 

  12. Kupferman, O., Morgenstern, G., Murano, A.: Typeness for omega-regular automata. Int. J. Found. Comput. Sci. 17(4), 869–884 (2006)

    Article  MATH  Google Scholar 

  13. Löding, C.: Efficient minimization of deterministic weak omega-automata. Inf. Process. Lett. 79(3), 105–109 (2001)

    Article  MATH  Google Scholar 

  14. Piterman, N., Pnueli, A., Sa’ar, Y.: Synthesis of reactive(1) designs. In: Emerson, E.A., Namjoshi, K.S. (eds.) VMCAI 2006. LNCS, vol. 3855, pp. 364–380. Springer, Heidelberg (2005)

    Chapter  Google Scholar 

  15. Pnueli, A., Rosner, R.: On the synthesis of a reactive module. In: POPL, pp. 179–190 (1989)

    Google Scholar 

  16. Sakallah, K.A.: Symmetry and Satisfiability. In: [5], pp. 289–338 (2009)

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Reactive Systems Group, Saarland University, Germany

    Rüdiger Ehlers

Authors
  1. Rüdiger Ehlers
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. Technion, Technion City, 32000, Haifa, Israel

    Ofer Strichman

  2. Vienna University of Technology, Favoritenstr. 9-11, 1040, Vienna, Austria

    Stefan Szeider

Rights and permissions

Reprints and permissions

Copyright information

© 2010 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Ehlers, R. (2010). Minimising Deterministic Büchi Automata Precisely Using SAT Solving. In: Strichman, O., Szeider, S. (eds) Theory and Applications of Satisfiability Testing – SAT 2010. SAT 2010. Lecture Notes in Computer Science, vol 6175. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-14186-7_28

Download citation

  • DOI: https://doi.org/10.1007/978-3-642-14186-7_28

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-642-14185-0

  • Online ISBN: 978-3-642-14186-7

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation