On Complementing Nondeterministic Büchi Automata

  • Sankar Gurumurthy
  • Orna Kupferman
  • Fabio Somenzi
  • Moshe Y. Vardi
Part of the Lecture Notes in Computer Science book series (LNCS, volume 2860)


Several optimal algorithms have been proposed for the complementation of nondeterministic Büchi word automata. Due to the intricacy of the problem and the exponential blow-up that complementation involves, these algorithms have never been used in practice, even though an effective complementation construction would be of significant practical value. Recently, Kupferman and Vardi described a complementation algorithm that goes through weak alternating automata and that seems simpler than previous algorithms. We combine their algorithm with known and new minimization techniques. Our approach is based on optimizations of both the intermediate weak alternating automaton and the final nondeterministic automaton, and involves techniques of rank and height reductions, as well as direct and fair simulation.


Model Check Temporal Logic Direct Simulation Acceptance Condition Simulation Relation 
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.


  1. 1.
    Alpern, B., Schneider, F.B.: Recognizing safety and liveness. Distributed Computing 2, 117–126 (1987)MATHCrossRefGoogle Scholar
  2. 2.
    Alur, R., Henzinger, T.A., Kupferman, O., Vardi, M.Y.: Alternating refinement relations. In: Sangiorgi, D., de Simone, R. (eds.) CONCUR 1998. LNCS, vol. 1466, pp. 163–178. Springer, Heidelberg (1998)CrossRefGoogle Scholar
  3. 3.
    Armoni, R., Fix, L., Flaisher, A., Gerth, R., Ginsburg, B., Kanza, T., Landver, A., Mador-Haim, S., Singerman, E., Tiemeyer, A., Vardi, M.Y., Zbar, Y.: The ForSpec temporal logic: A new temporal property-specification language. In: Katoen, J.-P., Stevens, P. (eds.) TACAS 2002. LNCS, vol. 2280, pp. 296–311. Springer, Heidelberg (2002)CrossRefGoogle Scholar
  4. 4.
    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)CrossRefGoogle Scholar
  5. 5.
    Büchi, J.R.: On a decision method in restricted second order arithmetic. In: 1960 International Congress on Logic, Methodology, and Philosophy of Science, pp. 1–11. Stanford University Press (1962)Google Scholar
  6. 6.
    Chandra, K., Kozen, D.C., Stockmeyer, L.J.: Alternation. JACM 28(1), 114–133 (1981)MATHCrossRefMathSciNetGoogle Scholar
  7. 7.
    Fritz, C., Wilke, T.: State space reductions for alternating Büchi automata. In: Agrawal, M., Seth, A.K. (eds.) FSTTCS 2002. LNCS, vol. 2556, pp. 157–168. Springer, Heidelberg (2002)CrossRefGoogle Scholar
  8. 8.
    Gurumurthy, S., Bloem, R., Somenzi, F.: Fair simulation minimization. In: Brinksma, E., Larsen, K.G. (eds.) CAV 2002. LNCS, vol. 2404, pp. 610–623. Springer, Heidelberg (2002)CrossRefGoogle Scholar
  9. 9.
    Holzmann, G.J.: Design and Validation of Computer Protocols. Prentice-Hall, Englewood Cliffs (1991)Google Scholar
  10. 10.
    Klarlund, N.: Progress measures for complementation of ω-automata with application to temporal logic. In: FOCS, pp. 358–367 (1991)Google Scholar
  11. 11.
    Kupferman, O., Vardi, M.Y.: Relating linear and branching model checking. In: IFIP PROCOMET, pp. 304–326 (1998)Google Scholar
  12. 12.
    Kupferman, O., Vardi, M.Y.: Weak alternating automata are not that weak. ACM TOCL 2(3), 408–429 (2001)MATHCrossRefMathSciNetGoogle Scholar
  13. 13.
    Kurshan, R.P.: Complementing deterministic Büchi automata in polynomial time. Journal of Computer and System Sciences 35, 59–71 (1987)MATHCrossRefMathSciNetGoogle Scholar
  14. 14.
    Kurshan, R.P.: Computer-AidedVerification of Coordinating Processes. Princeton University Press, Princeton (1994)Google Scholar
  15. 15.
    Lichtenstein, O., Pnueli, A.: Checking that finite state concurrent programs satisfy their linear specification. In: POPL, pp. 97–107 (1985)Google Scholar
  16. 16.
    Löding, C., Thomas, W.: Alternating automata and logics over infinite words. In: Watanabe, O., Hagiya, M., Ito, T., van Leeuwen, J., Mosses, P.D. (eds.) TCS 2000. LNCS, vol. 1872, pp. 521–535. Springer, Heidelberg (2000)CrossRefGoogle Scholar
  17. 17.
    Maidl, M.: The common fragment of CTL and LTL. In: FOCS, pp. 643–652 (2000)Google Scholar
  18. 18.
    Michel, M.: Complementation is more difficult with automata on infinite words. In: CNET, Paris (1988) (manuscript)Google Scholar
  19. 19.
    Miyano, S., Hayashi, T.: Alternating finite automata on ω-words. TCS 32, 321–330 (1984)MATHCrossRefMathSciNetGoogle Scholar
  20. 20.
    Safra, S.: On the complexity of ω-automata. In: FOCS, pp. 319–327 (1988)Google Scholar
  21. 21.
    Sistla, P.A.: Safety, liveness and fairness in temporal logic. Formal Aspects in Computing 6, 495–511 (1994)MATHCrossRefGoogle Scholar
  22. 22.
    Sistla, P.A., Vardi, M.Y., Wolper, P.: The complementation problem for Büchi automata with applications to temporal logic. TCS 49, 217–237 (1987)MATHCrossRefMathSciNetGoogle Scholar
  23. 23.
    Somenzi, F., Bloem, R.: Efficient Büchi automata from LTL formulae. In: Emerson, E.A., Sistla, A.P. (eds.) CAV 2000. LNCS, vol. 1855, pp. 248–263. Springer, Heidelberg (2000)CrossRefGoogle Scholar
  24. 24.
    Tasiran, S., Hojati, R., Brayton, R.K.: Language containment using non-deterministic omega-automata. In: Camurati, P.E., Eveking, H. (eds.) CHARME 1995. LNCS, vol. 987, pp. 261–277. Springer, Heidelberg (1995)Google Scholar
  25. 25.
    Vardi, M.Y., Wolper, P.: An automata-theoretic approach to automatic program verification. In: LICS, pp. 322–331 (1986)Google Scholar
  26. 26.
    Wolper, P.: Temporal logic can be more expressive. I&C 56(1–2), 72–99 (1983)MATHMathSciNetGoogle Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2003

Authors and Affiliations

  • Sankar Gurumurthy
    • 1
  • Orna Kupferman
    • 2
  • Fabio Somenzi
    • 1
  • Moshe Y. Vardi
    • 3
  1. 1.University of Colorado at Boulder 
  2. 2.Hebrew University 
  3. 3.Rice University 

Personalised recommendations