Temporal logics over linear time domains are in PSPACE. (English) Zbl 1280.68112
Summary: We investigate the complexity of the satisfiability problem of temporal logics with a finite set of modalities definable in the existential fragment of monadic second-order logic. We show that the problem is in PSPACE over the class of all linear orders. The same techniques show that the problem is in PSPACE over many interesting classes of linear orders.
MSC:
| 68Q25 | Analysis of algorithms and problem complexity |
| 03B44 | Temporal logic |
| 68Q15 | Complexity classes (hierarchies, relations among complexity classes, etc.) |
References:
| [1] | Bedon, N.; Bes, A.; Carton, O.; Rispal, C., Logic and rational languages of words indexed by linear orderings, (CSR 2008. CSR 2008, LNCS, vol. 5010 (2008)), 76-85 · Zbl 1142.03346 |
| [2] | Bruyère, V.; Carton, O., Automata on linear orderings, (MFCS 2001. MFCS 2001, LNCS, vol. 2136 (2001)), 236-247 · Zbl 0999.68100 |
| [3] | Büchi, J. R., On a decision method in restricted second order arithmetic, (Logic, Methodology and Philosophy of Science (1962), Stanford University Press), 1-11 · Zbl 0147.25103 |
| [4] | Büchi, J. R.; Siefkes, D., The Monadic Second-order Theory of all Countable Ordinals, Springer Lecture Notes, vol. 328 (1973) · Zbl 0298.02050 |
| [5] | 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 |
| [6] | J. Cristau, Automata and temporal logic over arbitrary linear time, in: FSTTCS 2009, LIPIcs 4, 2009, pp. 133-144.; J. Cristau, Automata and temporal logic over arbitrary linear time, in: FSTTCS 2009, LIPIcs 4, 2009, pp. 133-144. · Zbl 1248.68293 |
| [7] | S. Demri, A. Rabinovich, The complexity of temporal logic with until and since over ordinals, in: LPAR, 2007, pp. 531-545.; S. Demri, A. Rabinovich, The complexity of temporal logic with until and since over ordinals, in: LPAR, 2007, pp. 531-545. · Zbl 1137.03308 |
| [8] | Feferman, S.; Vaught, R. L., The first-order properties of products of algebraic systems, Fund. Math., 47, 57-103 (1959) · Zbl 0088.24803 |
| [9] | D.M. Gabbay, A. Pnueli, S. Shelah, J. Stavi, On the temporal analysis of fairness, in: 7th POPL, 1980, pp. 163-173.; D.M. Gabbay, A. Pnueli, S. Shelah, J. Stavi, On the temporal analysis of fairness, in: 7th POPL, 1980, pp. 163-173. |
| [10] | Gabbay, D. M.; Hodkinson, I.; Reynolds, M., Temporal Logics, vol. 1 (1994), Clarendon Press: Clarendon Press Oxford · Zbl 0921.03023 |
| [11] | Gurevich, Y., Monadic second-order theories, (Barwise, J.; Feferman, S., Model-Theoretic Logics (1985), Springer-Verlag), 479-506 |
| [12] | H. Kamp, Tense logic and the theory of linear order, PhD thesis, University of California, L.A., 1968.; H. Kamp, Tense logic and the theory of linear order, PhD thesis, University of California, L.A., 1968. |
| [13] | Läuchli, H.; Leonard, J., On the elementary theory of linear order, Fund. Math., 59, 109-116 (1966) · Zbl 0156.25301 |
| [14] | Rabin, M. O., Decidability of second-order theories and automata on infinite trees, Trans. Amer. Math. Soc., 141, 1-35 (1969) · Zbl 0221.02031 |
| [15] | Rabinovich, A., Temporal logics over linear time domains are in PSPACE, (LNCS, vol. 6227 (2010)), 29-50 · Zbl 1287.68081 |
| [16] | Reynolds, M., The complexity of the temporal logic with until over general linear time, J. Comput. System Sci., 66, 393-426 (2003) · Zbl 1019.03014 |
| [17] | Reynolds, M., The complexity of temporal logic over the reals, Ann. Pure Appl. Logic, 161, 8, 1063-1096 (2010) · Zbl 1235.03052 |
| [18] | Reynolds, M., The complexity of decision problems for linear temporal logics, J. Stud. Logic, 3, 1, 19-50 (2010) |
| [19] | Rispal, C.; Carton, O., Complementation of rational sets on countable scattered linear orderings, Internat. J. Found. Comput. Sci., 16, 4, 767-786 (2005) · Zbl 1161.68551 |
| [20] | Rosenstein, J. G., Linear Ordering (1982), Academic Press: Academic Press New York · Zbl 0179.01303 |
| [21] | Shelah, S., The monadic theory of order, Ann. of Math., 102, 349-419 (1975) · Zbl 0345.02034 |
| [22] | Sistla, A. P.; Clarke, E. M., The complexity of propositional linear temporal logics, J. ACM, 32, 3, 733-749 (1985) · Zbl 0632.68034 |
| [23] | Thomas, W., Ehrenfeucht games, the composition method, and the monadic theory of ordinal words, (Structures in Logic and Computer Science: A Selection of Essays in Honor of A. Ehrenfeucht. Structures in Logic and Computer Science: A Selection of Essays in Honor of A. Ehrenfeucht, LNCS, vol. 1261 (1997)), 118-143 · Zbl 0888.03002 |
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.
