Complementation Constructions for Nondeterministic Automata on Infinite Words

  • Orna Kupferman
  • Moshe Y. Vardi
Part of the Lecture Notes in Computer Science book series (LNCS, volume 3440)


The complementation problem for nondeterministic automata on infinite words has numerous applications in formal verification. In particular, the language-containment problem, to which many verification problems are reduced, involves complementation. Traditional optimal complementation constructions are quite complicated and have not been implemented. Recently, we have developed an analysis techniques for runs of co-Büchi and generalized co-Büchi automata and used the analysis to describe simpler optimal complementation constructions for Büchi and generalized Büchi automata. In this work, we extend the analysis technique to Rabin and Streett automata, and use the analysis to describe novel and simple complementation constructions for them.


Level Ranking Acceptance Condition Complementation Problem Deterministic Automaton Nondeterministic Automaton 
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. [AL91]
    Abadi, M., Lamport, L.: The existence of refinement mappings. TCS 82(2), 253–284 (1991)zbMATHCrossRefMathSciNetGoogle Scholar
  2. [Att99]
    Attie, P.: Liveness-preserving simulation relations. In: Proc. 18th PODC, pp. 63–72 (1999)Google Scholar
  3. [Büc62]
    Büchi, J.R.: On a decision method in restricted second order arithmetic. In: Proc. Internat. Congr. Logic, Method. and Philos. Sci. 1960, Stanford, pp. 1–12 (1962)Google Scholar
  4. [Cho74]
    Choueka, Y.: Theories of automata on ω-tapes: A simplified approach. Journal of CSS 8, 117–141 (1974)zbMATHMathSciNetGoogle Scholar
  5. [DHW91]
    Dill, D.L., Hu, A.J., Wong-Toi, H.: Checking for language inclusion using simulation relations. In: Larsen, K.G., Skou, A. (eds.) CAV 1991. LNCS, vol. 575, pp. 255–265. Springer, Heidelberg (1991)Google Scholar
  6. [EJ91]
    Emerson, E.A., Jutla, C.: Tree automata, μ-calculus and determinacy. In: Proc. 32nd FOCS, pp. 368–377 (1991)Google Scholar
  7. [EKM98]
    Elgaard, J., Klarlund, N., Möller, A.: Mona 1.x: new techniques for WS1S and WS2S. In: Y. Vardi, M. (ed.) CAV 1998. LNCS, vol. 1427, pp. 516–520. Springer, Heidelberg (1998)CrossRefGoogle Scholar
  8. [FKV04]
    Friedgut, E., Kupferman, O., Vardi, M.Y.: Büchi complementation made tighter. In: Wang, F. (ed.) ATVA 2004. LNCS, vol. 3299, pp. 64–78. Springer, Heidelberg (2004)CrossRefGoogle Scholar
  9. [GBS02]
    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
  10. [GKSV03]
    Gurumurthy, S., Kupferman, O., Somenzi, F., Vardi, M.Y.: On complementing nondeterministic Büchi automata. In: Geist, D., Tronci, E. (eds.) CHARME 2003. LNCS, vol. 2860, pp. 96–110. Springer, Heidelberg (2003)CrossRefGoogle Scholar
  11. [HHK95]
    Henzinger, M.R., Henzinger, T.A., Kopke, P.W.: Computing simulations on finite and infinite graphs. In: Proc. 36th FOCS, pp. 453–462 (1995)Google Scholar
  12. [HHK96]
    Hardin, R.H., Har’el, Z., Kurshan, R.P.: COSPAN. In: Alur, R., Henzinger, T.A. (eds.) CAV 1996. LNCS, vol. 1102, pp. 423–427. Springer, Heidelberg (1996)Google Scholar
  13. [HK02]
    Harel, D., Kupferman, O.: On the behavioral inheritance of state-based objects. IEEE TSE 28(9), 889–903 (2002)Google Scholar
  14. [HKR02]
    Henzinger, T.A., Kupferman, O., Rajamani, S.: Fair simulation. I&C 173(1), 64–81 (2002)zbMATHMathSciNetGoogle Scholar
  15. [Hol97]
    Holzmann, G.J.: The model checker SPIN. IEEE TSE 23(5), 279–295 (1997)MathSciNetGoogle Scholar
  16. [Kla90]
    Klarlund, N.: Progress Measures and finite arguments for infinite computations. PhD thesis, Cornell University (1990)Google Scholar
  17. [Kla91]
    Klarlund, N.: Progress measures for complementation of ω-automata with applications to temporal logic. In: Proc. 32nd FOCS, pp. 358–367 (1991)Google Scholar
  18. [KP00]
    Kesten, Y., Pnueli, A.: Verification by augmented finitary abstraction. I&C 163(1), 203–243 (2000)zbMATHMathSciNetGoogle Scholar
  19. [KPP03]
    Kesten, Y., Piterman, N., Pnueli, A.: Bridging the gap between fair simulation and trace containment. In: Hunt Jr., W.A., Somenzi, F. (eds.) CAV 2003. LNCS, vol. 2725, pp. 381–393. Springer, Heidelberg (2003)CrossRefGoogle Scholar
  20. [KPSZ02]
    Kesten, Y., Pnueli, A., Shahar, E., Zuck, L.: Network invariant in action. In: Brim, L., Jančar, P., Křetínský, M., Kucera, A. (eds.) CONCUR 2002. LNCS, vol. 2421, pp. 101–115. Springer, Heidelberg (2002)CrossRefGoogle Scholar
  21. [Kur87]
    Kurshan, R.P.: Complementing deterministic Büchi automata in polynomial time. Journal of CSS 35, 59–71 (1987)zbMATHMathSciNetGoogle Scholar
  22. [Kur94]
    Kurshan, R.P.: Computer Aided Verification of Coordinating Processes. Princeton Univ. Press, Princeton (1994)Google Scholar
  23. [KV01]
    Kupferman, O., Vardi, M.Y.: Weak alternating automata are not that weak. ACM ToCL 2, 408–429 (2001)zbMATHCrossRefMathSciNetGoogle Scholar
  24. [KV04]
    Kupferman, O., Vardi, M.Y.: From complementation to certification. In: Jensen, K., Podelski, A. (eds.) TACAS 2004. LNCS, vol. 2988, pp. 591–606. Springer, Heidelberg (2004)CrossRefGoogle Scholar
  25. [LPS81]
    Lehman, D., Pnueli, A., Stavi, J.: Impartiality, justice, and fairness – the ethics of concurrent termination. In: Even, S., Kariv, O. (eds.) ICALP 1981. LNCS, vol. 115, pp. 264–277. Springer, Heidelberg (1981)Google Scholar
  26. [LT87]
    Lynch, N.A., Tuttle, M.R.: Hierarchical correctness proofs for distributed algorithms. In: Proc. 6th PODC, pp. 137–151 (1987)Google Scholar
  27. [Mer00]
    Merz, S.: Weak alternating automata in Isabelle/HOL. In: Aagaard, M.D., Harrison, J. (eds.) TPHOLs 2000. LNCS, vol. 1869, pp. 423–440. Springer, Heidelberg (2000)CrossRefGoogle Scholar
  28. [Mic88]
    Michel, M.: Complementation is more difficult with automata on infinite words. CNET, Paris (1988)Google Scholar
  29. [MS73]
    Meyer, A.R., Stockmeyer, L.J.: Word problems requiring exponential time: Preliminary report. In: Proc. 5th STOC, pp. 1–9 (1973)Google Scholar
  30. [MS87]
    Muller, D.E., Schupp, P.E.: Alternating automata on infinite trees. TCS 54, 267–276 (1987)zbMATHCrossRefMathSciNetGoogle Scholar
  31. [RS59]
    Rabin, M.O., Scott, D.: Finite automata and their decision problems. IBM Journal of Research and Development 3, 115–125 (1959)CrossRefMathSciNetGoogle Scholar
  32. [Saf88]
    Safra, S.: On the complexity of ω-automata. In: 29th FOCS, pp. 319–327 (1988)Google Scholar
  33. [Saf92]
    Safra, S.: Exponential determinization for ω-automata with strong-fairness acceptance condition. In: Proc. 24th STOC (1992)Google Scholar
  34. [SV89]
    Safra, S., Vardi, M.Y.: On ω-automata and temporal logic. In: Proc. 21st STOC, pp. 127–137 (1989)Google Scholar
  35. [THB95]
    Tasiran, S., Hojati, R., Brayton, R.K.: Language containment using non-deterministic ω-automata. In: Camurati, P.E., Eveking, H. (eds.) CHARME 1995. LNCS, vol. 987, pp. 261–277. Springer, Heidelberg (1995)Google Scholar
  36. [VW94]
    Vardi, M.Y., Wolper, P.: Reasoning about infinite computations. I&C 115(1), 1–37 (1994)zbMATHMathSciNetGoogle Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2005

Authors and Affiliations

  • Orna Kupferman
    • 1
  • Moshe Y. Vardi
    • 2
  1. 1.School of Engineering and Computer ScienceHebrew UniversityJerusalemIsrael
  2. 2.Department of Computer ScienceRice UniversityHoustonU.S.A

Personalised recommendations