The complexity of temporal logic over the reals. (English) Zbl 1235.03052
Summary: It is shown that the decision problem for the temporal logic with until and since connectives over real-numbers time is PSPACE-complete. This is the most practically useful dense time temporal logic.
MSC:
| 03B44 | Temporal logic |
| 68Q17 | Computational difficulty of problems (lower bounds, completeness, difficulty of approximation, etc.) |
References:
| [1] | Alur, R.; Henzinger, T. A., Real-time logics: Complexity and expressiveness, Inf. Control, 104, 35-77 (1993) · Zbl 0791.68103 |
| [2] | Burgess, J. P.; Gurevich, Y., The decision problem for linear temporal logic, Notre Dame J. Form. Log., 26, 2, 115-128 (1985) · Zbl 0573.03004 |
| [3] | Gabbay, D. M.; Hodkinson, I. M., An axiomatisation of the temporal logic with until and since over the real numbers, J. Logic Comput., 1, 2, 229-260 (1990) · Zbl 0744.03018 |
| [4] | Gabbay, D.; Hodkinson, I.; Reynolds, M., Temporal Logic: Mathematical Foundations and Computational Aspects, vol. 1 (1994), Oxford University Press · Zbl 0921.03023 |
| [5] | Hodkinson, I. M., Complexity of monodic guarded fragments over linear and real time, Ann. Pure Appl. Logic, 138, 1-3, 94-125 (2006) · Zbl 1093.03009 |
| [6] | Hirshfeld, Y.; Rabinovich, A., Timer formulas and decidable metric temporal logic, Inform. and Comput., 198, 2, 148-178 (2005) · Zbl 1068.03014 |
| [7] | Halpern, J.; Shoham, Y., A propositional modal logic of time intervals, (Proceedings, Symposium on Logic in Computer Science (1986), IEEE: IEEE Boston) · Zbl 0799.68175 |
| [8] | Hopcroft, J.; Ullman, J., Introduction to Automata Theory, Languages, and Computation (1979), Addison-Wesley · Zbl 0426.68001 |
| [9] | H. Kamp, Tense logic and the theory of linear order, Ph.D. Thesis, University of California, Los Angeles, 1968.; H. Kamp, Tense logic and the theory of linear order, Ph.D. Thesis, University of California, Los Angeles, 1968. |
| [10] | Kesten, Y.; Manna, Z.; Pnueli, A., Temporal verification of simulation and refinement, (de Bakker, J.; de Roover, W.; Rozenberg, G., A Decade of Concurrency: Reflections and Perspectives: REX School/Symposium. A Decade of Concurrency: Reflections and Perspectives: REX School/Symposium, Noordwijkerhout, The Netherlands, June 1-4, 1993 (1994), Springer-Verlag), 273-346 |
| [11] | Läuchli, H.; Leonard, J., On the elementary theory of linear order, Fund. Math., 59, 109-116 (1966) · Zbl 0156.25301 |
| [12] | Marx, M.; Mikulas, S.; Reynolds, M., The mosaic method for temporal logics, (Dyckhoff, R., Automated Reasoning with Analytic Tableaux and Related Methods, Proceedings of International Conference. Automated Reasoning with Analytic Tableaux and Related Methods, Proceedings of International Conference, TABLEAUX 2000, Saint Andrews, Scotland, July 2000 (2000), Springer), 324-340 · Zbl 0963.03025 |
| [13] | Németi, I., Decidable versions of first order logic and cylindric-relativized set algebras, (Csirmaz, L.; Gabbay, D.; de Rijke, M., Logic Colloquium’92 (1995), CSLI Publications), 171-241 · Zbl 0852.03002 |
| [14] | A. Pnueli, The temporal logic of programs, in: Proceedings of the Eighteenth Symposium on Foundations of Computer Science, Providence, RI, 1977, pp. 46-57.; A. Pnueli, The temporal logic of programs, in: Proceedings of the Eighteenth Symposium on Foundations of Computer Science, Providence, RI, 1977, pp. 46-57. |
| [15] | V.R. Pratt, Models of program logics, in: Proc. 20th IEEE. Symposium on Foundations of Computer Science, San Juan, 1979, pp. 115-122.; V.R. Pratt, Models of program logics, in: Proc. 20th IEEE. Symposium on Foundations of Computer Science, San Juan, 1979, pp. 115-122. |
| [16] | Rabin, M. O., Decidability of second order theories and automata on infinite trees, Amer. Math. Soc. Trans., 141, 1-35 (1969) · Zbl 0221.02031 |
| [17] | Rabinovich, A., On the decidability of continuous time specification formalisms, J. Logic Comput., 8, 669-678 (1998) · Zbl 0913.03018 |
| [18] | Reynolds, M., An axiomatization for Until and Since over the reals without the IRR rule, Studia Logica, 51, May, 165-193 (1992) · Zbl 0785.03006 |
| [19] | Reynolds, M., Continuous temporal models, (Brooks, M.; Corbett, D.; Stumptner, M., Advances in Artificial Intelligence, Proceedings of the 14th Australian Joint Conference on Artificial Intelligence. Advances in Artificial Intelligence, Proceedings of the 14th Australian Joint Conference on Artificial Intelligence, AI’2001, Adelaide, December 2001. Advances in Artificial Intelligence, Proceedings of the 14th Australian Joint Conference on Artificial Intelligence. Advances in Artificial Intelligence, Proceedings of the 14th Australian Joint Conference on Artificial Intelligence, AI’2001, Adelaide, December 2001, Lecture Notes in A.I., vol. 2256 (2001), Springer-Verlag), 414-425 · Zbl 1052.03521 |
| [20] | Reynolds, M., The complexity of the temporal logic with until over general linear time, J. Comput. Syst. Sci., 66, 393-426 (2003) · Zbl 1019.03014 |
| [21] | Savitch, W. J., Relationships between non-deterministic and deterministic tape complexities, J. Comput. Syst. Sci., 4, 177-192 (1970) · Zbl 0188.33502 |
| [22] | Sistla, A.; Clarke, E., Complexity of propositional linear temporal logics, J. ACM, 32, 733-749 (1985) · Zbl 0632.68034 |
| [23] | Sistla, A.; Zuck, L., Reasoning in a restricted temporal logic, Inform. and Comput., 102, 167-195 (1993) · Zbl 0771.03007 |
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.
