Skip to main content
SpringerLink
Log in
Book cover

International Colloquium on Automata, Languages, and Programming

ICALP 1985: Automata, Languages and Programming pp 465–474Cite as

The complementation problem for Büchi automata with applications to temporal logic

  • Conference paper
  • First Online:

Part of the book series: Lecture Notes in Computer Science ((LNCS,volume 194))

Abstract

The problem of complementing Büchi automata arises when developing procedures for temporal logics of programs. Unfortunately, previously known constructions for complementing Büchi automata involve a doubly exponential blow-up in the size of the automaton. We present a construction that involves only an exponential blow-up. We use this construction to prove a polynomial space upper bound for the propositional temporal logic of regular events and to prove a complexity hierarchy result for quantified propositional temporal logic.

extended abstract

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

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

5. References

  1. H. Alaiwan, “Equivalence of Infinite Behavior of Finite Automata”, Theoretical Computer Science 31(1984), pp. 297–306.

    Article  Google Scholar 

  2. J. R. Büchi, “On a Decision Method in Restricted Second Order Arithmetic”, Proc. Internat. Congr. Logic, Method and Philos. Sci. 1960, Stanford University Press, 1962, pp. 1–12.

    Google Scholar 

  3. J. R. Büchi, “The Monadic Theory of ω1”, In Decidable Theories II, Lecture Notes in Mathematics, v. 328, Springer-Verlag, 1973, pp. 1–127.

    Google Scholar 

  4. Y. Choueka, “Theories of Automata on ω-Tapes: A Simplified Approach”, J. Computer and System Sciences, 8 (1974), pp. 117–141.

    Google Scholar 

  5. S. Eilenberg, Automata, Languages and Machines, vol. A, Academic Press, New York, 1974.

    Google Scholar 

  6. D. Harel, D. Kozen, R. Parikh, “Process Logic Expressiveness, Decidability, Completeness”, Journal of Computer and System Science 25, 2 (1982), pp. 144–170.

    Article  Google Scholar 

  7. R. McNaughton, “Testing and Generating Infinite Sequences by a Finite Automaton”, Information and Control 9 (1966), pp. 521–530

    Google Scholar 

  8. A. R. Meyer, “Weak Monadic Second Order Theory of Successor is not Elementary Recursive”, Proc. Logic Colloquium, Lecture Notes in Mathematics, v. 453, Springer-Verlag, 1975, pp. 132–154.

    Google Scholar 

  9. A. R. Meyer, L. J. Stockmeyer, “The Equivalence Problem for Regular Expressions with Squaring Requires Exponential Time”, Proc. 13th IEEE Symp. on Switching and Automata Theory, Long Beach, CA, 1972, pp. 125–129.

    Google Scholar 

  10. H. Nishimura, “Descriptively Complete Process Logic”, Acta Informatica, 14 (1980), pp. 359–369.

    Article  Google Scholar 

  11. A. Pnueli, “The Temporal Logic of Concurrent Programs”, Theoretical Computer Science 13(1981), pp. 45–60.

    Article  Google Scholar 

  12. M.O. Rabin, “Decidability of Second Order Theories and Automata on Infinite Trees”, Trans. AMS, 141(1969), pp. 1–35.

    Google Scholar 

  13. M.O. Rabin, “Weakly Definable Relations and Special Automata”, Proc. Symp. Math. Logic and Foundations of Set Theory (Y. Bar-Hillel, ed.), North-Holland, 1970, pp. 1–23.

    Google Scholar 

  14. E. L. Robertson, “Structure of Complexity in the Weak Monadic Second-Order Theory of the Natural Numbers”, Proc. 6th ACM Symp. on Theory of Computing, Seattle, 1974, pp. 161–171.

    Google Scholar 

  15. M. O. Rabin, D. Scott, “Finite Automata and their Decision Problems”, IBM J. Res. & Dev., 3(2), 1959, pp 114–125.

    Google Scholar 

  16. A.P. Sistla, E.M. Clarke, “The Complexity of Propositional Linear Time Logics”, Proc. 14th ACM Symp. on Theory of Computing, San Francisco, 1982, pp. 159–168, to appear in J. ACM.

    Google Scholar 

  17. D. Siefkes, Decidable Theories I — Büchi's Monadic Second-Order Successor Arithmetics, Lecture Notes in Mathematics, v. 120, Springer-Verlag, 1970.

    Google Scholar 

  18. A. P. Sistla, Theoretical Issues in The Design and Verification of Distributed Systems, Ph.D. Thesis, Harvard University, 1983.

    Google Scholar 

  19. B. A. Trakhtenbrot, Y. M. Barzdin, Finite Automata Behavior and Synthesis, North Holland, Amsterdam, 1973.

    Google Scholar 

  20. M.Y. Vardi, “On deterministic ω-automata”, to appear.

    Google Scholar 

  21. M.Y. Vardi, L. Stockmeyer, “Improved Upper and Lower Bounds for Modal Logics of Programs”, Proc. 17 ACM Symp. on Theory of Computing, Providence, May 1985.

    Google Scholar 

  22. M. Y. Vardi, P. Wolper, “Yet Another Process Logic”, in Logics of Programs, Springer-Verlag Lecture Notes in Computer Science, vol. 164, Berlin, 1983, pp. 501–512.

    Google Scholar 

  23. M. Y. Vardi, P. Wolper, “Automata Theoretic Techniques for Modal Logics of Programs”, IBM Research Report, October 1984. A preleminary version appeared in Proc. ACM Symp. on Theory of Computing, Washington, April 1984, pp. 446–456.

    Google Scholar 

  24. P. Wolper, M. Y. Vardi, A. P. Sistla, “Reasoning about Infinite Computation Paths”, Proc. 24th IEEE Symp. on Foundations of Computer Science, Tucson, 1983, pp. 185–194.

    Google Scholar 

  25. P. Wolper, “Synthesis of Communicating Processes from Temporal Logic Specifications”, Ph. D. Thesis, Stanford University, 1982.

    Google Scholar 

  26. P. Wolper, “Temporal Logic Can Be More Expressive”, Information and Control, 56(1983), pp. 72–99.

    Article  Google Scholar 

Download references

Author information

Authors and Affiliations

  1. University of Massachusetts, USA

    A. Prasad Sistla

  2. Stanford University, USA

    Moshe Y. Vardi

  3. AT&T Bell Laboratories, USA

    Pierre Wolper

Authors
  1. A. Prasad Sistla
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Moshe Y. Vardi
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. Pierre Wolper
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Wilfried Brauer

Rights and permissions

Reprints and permissions

Copyright information

© 1985 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Sistla, A.P., Vardi, M.Y., Wolper, P. (1985). The complementation problem for Büchi automata with applications to temporal logic. In: Brauer, W. (eds) Automata, Languages and Programming. ICALP 1985. Lecture Notes in Computer Science, vol 194. Springer, Berlin, Heidelberg. https://doi.org/10.1007/BFb0015772

Download citation

  • DOI: https://doi.org/10.1007/BFb0015772

  • Published:

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-15650-5

  • Online ISBN: 978-3-540-39557-7

  • eBook Packages: Springer Book Archive

Publish with us

Policies and ethics

Search

Navigation