Abstract
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.
Chapter PDF
Similar content being viewed by others
Keywords
- 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.
References
Abadi, M., Lamport, L.: The existence of refinement mappings. TCS 82(2), 253–284 (1991)
Attie, P.: Liveness-preserving simulation relations. In: Proc. 18th PODC, pp. 63–72 (1999)
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)
Choueka, Y.: Theories of automata on ω-tapes: A simplified approach. Journal of CSS 8, 117–141 (1974)
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)
Emerson, E.A., Jutla, C.: Tree automata, μ-calculus and determinacy. In: Proc. 32nd FOCS, pp. 368–377 (1991)
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)
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)
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)
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)
Henzinger, M.R., Henzinger, T.A., Kopke, P.W.: Computing simulations on finite and infinite graphs. In: Proc. 36th FOCS, pp. 453–462 (1995)
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)
Harel, D., Kupferman, O.: On the behavioral inheritance of state-based objects. IEEE TSE 28(9), 889–903 (2002)
Henzinger, T.A., Kupferman, O., Rajamani, S.: Fair simulation. I&C 173(1), 64–81 (2002)
Holzmann, G.J.: The model checker SPIN. IEEE TSE 23(5), 279–295 (1997)
Klarlund, N.: Progress Measures and finite arguments for infinite computations. PhD thesis, Cornell University (1990)
Klarlund, N.: Progress measures for complementation of ω-automata with applications to temporal logic. In: Proc. 32nd FOCS, pp. 358–367 (1991)
Kesten, Y., Pnueli, A.: Verification by augmented finitary abstraction. I&C 163(1), 203–243 (2000)
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)
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)
Kurshan, R.P.: Complementing deterministic Büchi automata in polynomial time. Journal of CSS 35, 59–71 (1987)
Kurshan, R.P.: Computer Aided Verification of Coordinating Processes. Princeton Univ. Press, Princeton (1994)
Kupferman, O., Vardi, M.Y.: Weak alternating automata are not that weak. ACM ToCL 2, 408–429 (2001)
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)
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)
Lynch, N.A., Tuttle, M.R.: Hierarchical correctness proofs for distributed algorithms. In: Proc. 6th PODC, pp. 137–151 (1987)
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)
Michel, M.: Complementation is more difficult with automata on infinite words. CNET, Paris (1988)
Meyer, A.R., Stockmeyer, L.J.: Word problems requiring exponential time: Preliminary report. In: Proc. 5th STOC, pp. 1–9 (1973)
Muller, D.E., Schupp, P.E.: Alternating automata on infinite trees. TCS 54, 267–276 (1987)
Rabin, M.O., Scott, D.: Finite automata and their decision problems. IBM Journal of Research and Development 3, 115–125 (1959)
Safra, S.: On the complexity of ω-automata. In: 29th FOCS, pp. 319–327 (1988)
Safra, S.: Exponential determinization for ω-automata with strong-fairness acceptance condition. In: Proc. 24th STOC (1992)
Safra, S., Vardi, M.Y.: On ω-automata and temporal logic. In: Proc. 21st STOC, pp. 127–137 (1989)
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)
Vardi, M.Y., Wolper, P.: Reasoning about infinite computations. I&C 115(1), 1–37 (1994)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2005 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Kupferman, O., Vardi, M.Y. (2005). Complementation Constructions for Nondeterministic Automata on Infinite Words. In: Halbwachs, N., Zuck, L.D. (eds) Tools and Algorithms for the Construction and Analysis of Systems. TACAS 2005. Lecture Notes in Computer Science, vol 3440. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-31980-1_14
Download citation
DOI: https://doi.org/10.1007/978-3-540-31980-1_14
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-25333-4
Online ISBN: 978-3-540-31980-1
eBook Packages: Computer ScienceComputer Science (R0)