[en] We investigate extensions of temporal logic by connectives defined by finite automata on infinite words. We consider three different logics, corresponding to three different types of acceptance conditions (finite, looping, and repeating) for the automata. It turns out, however that these logics all have the same expressive power and that their decision problems are all PSPACE-complete. We also investigate connectives defined by alternating automata and show that they do not increase the expressive power of the logic or the complexity of the decision problem. (C) 1994 Academic Press, Inc.
Disciplines :
Mathematics Computer science
Author, co-author :
Vardi, Moshe Y.
Wolper, Pierre ; Université de Liège - ULiège > Dép. d'électric., électron. et informat. (Inst.Montefiore)
Language :
English
Title :
Reasoning about Infinite Computations
Publication date :
1994
Journal title :
Information and Computation
ISSN :
0890-5401
eISSN :
1090-2651
Publisher :
Academic Press, San Diego, United States - California
Alur, R., and Henzinger, T. (1990), Real-time logics: Complexity and expressiveness, in "Proceedings, 5th IEEE Symposium on Logic in Computer Science," pp. 390-401.
Banieqbal, B., and Barringer, H. (1989), Temporal logic with fixed points, in "Proceedings, Temporal Logic in Specification" (B. Banieqbal, H. Barringer, and A. Pnueli, Eds.), pp. 62-74, Lecture Notes in Computer Science, Vol.398, Springer-Verlag, Berlin/New York.
Barringer, H., Kuper, R., and Pnueli, A. (1985), A compositional temporal approach to a CSP-like language, in "Formal Methods of Programming" (E. J. Neuhold and G. Chroust, Eds.), pp. 207-227, North-Holland, Amsterdam.
Barringer, H., Kuiper, R., and Pnueli, A. (1986), A really abstract concurrent model and its temporal logic, in "Proceedings, 13th ACM Symposium on Principles of Programming Languages, St. Petersburg," pp. 173-183.
Banieqbal, B., Barringer, H., and Pnueli, A., Eds. (1989), "Temporal Logic in Specification," Lecture Notes in Computer Science, Vol. 398, Springer-Verlag, Berlin/New York.
Brzozowski, J. A., and Leiss, E. (1980), On equations for regular languages, finite automata, and sequential networks, Theoret. Comput. Sci. 10, 19-35.
Buchi, J. R. (1962), On a decision method in restricted second order arithmetic, in "Proceedings, International Congress on Logic, Methodology and Philosophy of Science, 1960," pp. 1-12, Stanford Univ. Press, Stanford, CA.
Choueka, Y. (1974), Theories of automata on w-tapes: A simplified approach, J. Comput. System. Sci. 8, 117-141.
Chandra, A. K., Kozen, D. C., and Stockmeyer, L. J. (1981), Alternation, J. Assoc. Comput. Mach. 28, 114-133.
Emerson, E.A., and Clarke, E. M. (1981), Characterizing correctness properties of parallel programs as fixpoints, in "Proceedings, 7th International Colloquium on Automata, Languages and Programming," pp. 169-181, Lecture Notes in Computer Science, Vol. 85, Springer-Verlag, Berlin/New York.
Emerson, E. A., and Sistla, A. P. (1984), Deciding full branching time logic, Inform, and Control 61, 175-201.
Fischer, M., and Ladner, R. (1979), Propositional dynamic logic of regular programs, J. Comput. System Sci. 18, 194-211.
Gabbay, D., Pnueli, A., Shelah, S., and Stavi, J. (1980), The temporal analysis of fairness, in "Proceedings, 7th ACM Symposium on Principles of Programming Languages, Las Vegas," pp. 163-173.
Harel, D. (1979), "First Order Dynamic Logic," Lecture Notes in Computer Science, Vol. 68, Springer-Verlag, Berlin/New York.
Harel, D. (1984), Dynamic logic, in "Handbook of Philosophical Logic" (D. Gabbay and F. Guenther, Eds.), Vol. 2, pp. 497-604.
Harel, D., and Pratt, V. (1978), Nondeterminism in logics of programs, in "Proceedings, 5th ACM Symposium on Principles of Programming Languages, Tuscon," pp. 203-213.
Harel, D., Kozen, D., and Parikh, R. (1982), Processs logic: Expressiveness, decidability, completeness, J. Comput. System Sci. 25, 144-170.
Harel, D., and Peleg, D. (1985), Process logic with regular formulas, Theoret. Comput. Sci. 38, 307-322.
Harel, D., Rosner, R., and Vardi, M. Y. (1990), On the power of bounded concurrency. III. Reasoning about programs, in "Proceedings, 5th IEEE Symposium on Logic Computer Science," pp. 478-488.
Halpern, J. Y., and Reif, J. H. (1983), The Propositional dynamic logic of deterministic, well-structured programs, Theoret. Comput. Sci. 27, 127-165.
Harel, D., and Sherman, R. (1982), Looping vs repeating in dynamic logic, Inform. Control 55, 175-192.
Harel, D., and Sherman, R. (1985), Propositional dynamic logic of flowcharts, Inform, and Control 64, 119-135.
Jones, N. D. (1975), Space-bounded reducibility among combinatorial problems, J. Comput. System Sci. 11, 68-75.
Kaminski, M. (1985), A classification of co-regular languages, Theoret. Comput. Sci. 36, 217-229.
Kozen, D. (1983), Resuls on the propositional -calculus, Theoret. Comput. Sci. 27, 333-354.
Ladner, R. E. (1977), Application of model-theoretic games to discrete linear orders and finite automata, Inform, and Control 33, 281-303.
Lamport, L. (1977), Proving the correctness of multiprocess programs, IEEE Trans. Software Engrg. SE-7.
Landweber, L. H. (1969), Decision problems for co-automata, Math. Systems Theory 4, 376-384.
Leiss, E. (1981), Succinct representation of regular languages by Boolean automata, Theoret. Comput. Sci. 13, 323-330.
Lichtenstein, O., Pnueli, A., and Zuck, L. (1985), The glory of the past, in "Proceedings, Workshop on Logics of Programs, Brooklyn," pp. 196-218, Lecture Notes in Computer Science, Vol. 193, Springer-Verlag, Berlin/New York.
McNaughton, R. (1966), Testing and generating infinite sequences by a finite automaton, Inform, and Control 9, 521-530.
Meyer, A. R. (1975), Weak monadic second order theory of successor is not elementary recursive, in "Proceedings, Logic Colloquium," pp. 132-154, Vol.453, Springer-Verlag, Berlin/New York.
Smiyano, S., and Hayashi, T. (1984), Alternating automata on co-words, Theoret. Comput. Sci. 32, 321-330.
Milner, R. (1980), "A Calculus of Communicating Systems," Lecture Notes in Computer Science, Vol. 92, Springer-Verlag, Berlin/New York.
Muller, D. E., Saouidi, A., and Schupp, P. E. (1988), Weak alternating automata give a simple explanation of why most temporal and dynamic logics are decidable in exponential time, in "Proceedings, 3rd IEEE Symposium on Logic in Computer Science," pp. 422-427.
Meyer, A. R., and Stockmeyer, L. J. (1973), Non-elementary word problems in automata and logic, in "Proceedings, AMS Symposium on Complexity of Computation."
Manna, Z., and Pnueli, A. (1989), The anchored version of the temporal framework, in "Linear Time, Branching Time, and Partial Order in Logics and Models for Concurrency" (X. W. de Bakker, W. P. de Roever, and G. Rozenberg, Eds.), pp. 201-284, Lecture Notes in Computer Science, Vol. 354, Springer-Verlag, Berlin/New York.
Manna, Z., and Wolper, P. (1984), Synthesis of communicating processes from temporal logic specification, ACM Trans. Programming Languages Systems 6, pp. 68-93.
Muller, D. E. (1963), Infinite sequences and finite machines, in "Proceedings, 4th IEEE Symposium on Switching Circuit Theory and Logical Design, New York," pp. 3-16.
Moriya, T., and Yamusaki, H. (1988), Accepting conditions for automata on (languages, Theoret. Comput. Sci. 61, 137-147.
Nishimura, H. (198), Descriptively complete process logic. Acta Informat. 14, 359-369.
Pnueli, A. (1977), The temporal logic of programs, in "Proceedings, 8th IEEE Symposium on Foundations of Computer Science, Providence," pp. 46-57.
Pratt, V. R. (1976), Semantical considerations on Floyd-Hoare logic, in "Proceedings, 17th IEEE Symposium on Foundations of Computer Science," pp. 109-121.
Pratt, V. R. (1979), Models of program logics, in "Proceedings, 20th IEEE Symposium on Foundations of Computer Science, San Juan," pp. 115-122.
Pratt, V. R. (1980), A near-optimal method for reasoning about action, J. Comput. System Sci. 20, 231-254.
Pratt, V. R. (1981), Using graphs to understand PDL, in "Proceedings, Workshop on Logics of Programs, Yorktown Heights" (D. Kozen, Ed.), pp. 387-396, Lecture Notes in Computer Science, Vol.131, Springer-Verlag, Berlin/New York.
Pnueli, A., and Rosner, R. (1989), On the synthesis of a reactive module, in "Proceedings, 16th ACM Symposium on Principles of Programming Languages, Austin," pp. 179-190.
Rabin, M. O., and Scott, D. (1959), Finite automata and their decision problems, IBM J. Res. Dev. 3, 114-125.
Safra, S. (1988), On the complexity of ω-automata, in "Proceedings, 29th IEEE Symposium on Foundation of Computer Science," pp. 319-327.
Sistla, A. P., and Clarke, E. M. (1985), The complexity of propositional linear temporal logic, J. Assoc. Comput. Mach. 32, 733-749.
Shaw, A. C. (1979), "Software Specification Languages Based on Regular Expressions," Technical Report, Eidgenossische Technische Hochschule Zurich.
Sistla, A. P. (1983), "Theoretical Issues in The Design and Analysis of Distributed Systems," Ph.D. Thesis, Harvard University.
Streett, R. (1982), Propositional dynamic logic of looping and converse is elementarily decidable, Inform. Control 54, 121-141.
Streett, R. (1990), personal communication.
Staiger, L. (1987), Research in the theory of co-languages, Electron. Inf. Verar- beit. Kybernet. 23, 415-439.
Sistla, A. P., Vardi, M. Y., and Wolper, P. (1987), The complementation problem for Biichi automata with applications to temporal logic, Theoret. Comput. Sci. 49, 217-237.
Trakhtenbrot, B. A., and Barzdin, Y. M. (1973), "Finite Automata: Behavior and Synthesis," North-Holland, Amsterdam.
Thomas, W. (1979), Star-free regular sets of co-squences, Inform, and Control 42, 148-156.
Thomas, W. (1981), A combinatorial approach to the theory of cu-automata, Inform, and Control 48, 261-283.
Thomas, W. (1990), Automata on infinite objects, in "Handbook of Theoretical Computer Science," Vol. B (J. V. Leeuwen, Ed.), pp. 135-191, Elsevier, Amsterdam.
Vardi, M. Y., and Wolper, P. (1986), Automata-theoretic techniques for modal logic of programs, J. Comput. System Sci. 32, 183-221.
Vardi, M. Y., and Wolper, P. (1986), An automata-theoretic approach to automatic program verification, in "Proceedings, 1st IEEE Symposiums on Logic in Computer Science, Boston," pp. 332-334.
Vardi, M. Y. (1985), The taming of the converse: Reasoning about 2-way computations, in "Proceedings, Workshop on Logics of Programs, Brooklyn," pp. 413-424, Lecture Notes in Computer Science, Vol.193, Springer-Verlag, Berlin/New York.
Vardi, M. Y. (1985), Automatic verification of probabilistic concurrent finite- state programs, in "Proceedings, 26th IEEE Symposium on Foundations of Computer Science, Portland," pp. 327-338.
Vardi, M. Y. (1988), A temporal fixpoint calculus, in "Proceedings, 15th ACM Symposium on Principles of Programming Languages, San Diego," pp. 250-259.
Vardi, M. Y., and Wolper, P. (1983). Yet another process logic, in "Proceedings, Workshop on Logic of Programs," pp. 501-512, Lecture Notes in Computer Science, Vol. 164, Springer-Verlag, Berlin/New York.
Wagner, K. (1979), On co-regular sets, Inform, and Control 43, 123-177.
Wolper, P. (1982), "Synthesis of Communicating Processes from Temporal Logic Specifications," Ph.D. Thesis, Stanford University.
Wolper, P. (1983), Temporal logic can be more expressive, Inform, and Control 56, 72-99.
Wolper, P. (1989), On the relation of programs and computations to models of temporal logic, in "Proceedings, Temporal Logic in Specification" (B. Banieqbal, H. Barringer, and A. Pnueli, Eds.), pp. 75-123, Lecture Notes in Computer Science, Vol. 398, Springer-Verlag, Berlin/New York.
