×

The model checking fingerprints of CTL operators. (English) Zbl 1423.68288

Summary: The aim of this study is to understand the inherent expressive power of CTL operators. We investigate the complexity of model checking for all CTL fragments with one CTL operator and arbitrary Boolean operators. This gives us a fingerprint of each CTL operator. The comparison between the fingerprints yields a hierarchy of the operators that mirrors their strength with respect to model checking.

MSC:

68Q60 Specification and verification (program logics, model checking, etc.)
03B44 Temporal logic
PDFBibTeX XMLCite
Full Text: DOI arXiv

References:

[1] Alur, R., Henzinger, T.A., Kupferman, O.: Alternating-time temporal logic. J. ACM 49(5), 672-713 (2002). https://doi.org/10.1145/585265.585270 · Zbl 1326.68181 · doi:10.1145/585265.585270
[2] Bauland, M., Mundhenk, M., Schneider, T., Schnoor, H., Schnoor, I., Vollmer, H.: The tractability of model checking for LTL: the good, the bad, and the ugly fragments. TOCL 12(2), 26 (2011) · Zbl 1351.68151 · doi:10.1145/1877714.1877719
[3] Bauland, M., Schneider, T., Schnoor, H., Schnoor, I., Vollmer, H.: The complexity of generalized satisfiability for linear temporal logic. LMCS 5(1), 1-21 (2009) · Zbl 1183.03017
[4] Beyersdorff, O., Meier, A., Mundhenk, M., Schneider, T., Thomas, M., Vollmer, H.: Model checking CTL is almost always inherently sequential. LMCS 7(2), 1-21 (2011) · Zbl 1220.68068
[5] Böhler, E., Creignou, N., Reith, S., Vollmer, H.: Playing with boolean blocks, part I: Post’s lattice with applications to complexity theory. SIGACT 34(4), 38-52 (2003) · doi:10.1145/954092.954101
[6] Chandra, A.K., Kozen, D., Stockmeyer, L.J.: Alternation. J. ACM 28, 114-133 (1981) · Zbl 0473.68043 · doi:10.1145/322234.322243
[7] Chandra, A.K., Tompa, M.: The complexity of short two-person games. Discrete Appl. Math. 29(1), 21-33 (1990) · Zbl 0742.90089 · doi:10.1016/0166-218X(90)90080-V
[8] Clarke, E., Emerson, E.A., Sistla, A.P.: Automatic verification of finite-state concurrent systems using temporal logic specifications. TOPLAS 8(2), 244-263 (1986) · Zbl 0591.68027 · doi:10.1145/5397.5399
[9] Clarke, E.M., Emerson, E.A.: Design and synthesis of synchronisation skeletons using branching time temporal logic. In: Logic of Programs, LNCS, vol. 131, pp. 52-71. Springer (1981)
[10] Cook, S.A.: A taxonomy of problems with fast parallel algorithms. Inf. Control 64(1-3), 2-21 (1985) · Zbl 0575.68045 · doi:10.1016/S0019-9958(85)80041-3
[11] Emerson, E.A., Halpern, J.Y.: “Sometimes” and “not never” revisited: on branching versus linear time. J. ACM 33(1), 151-178 (1986) · Zbl 0629.68020 · doi:10.1145/4904.4999
[12] Emerson, E.A., Jutla, C.S.: The complexity of tree automata and logics of programs. SIAM J. Comput. 29(1), 132-158 (2000) · Zbl 0937.68074 · doi:10.1137/S0097539793304741
[13] Fischer, M.J., Ladner, R.E.: Propositional modal logic of programs. JCSS 18, 194-211 (1979) · Zbl 0408.03014
[14] Immerman, N.: Number of quantifiers is better than number of tape cells. J. Comput. Syst. Sci. 22(3), 384-406 (1981) · Zbl 0486.03019 · doi:10.1016/0022-0000(81)90039-8
[15] Krebs, A., Meier, A., Mundhenk, M.: The model checking fingerprints of CTL operators. In: Grandi, F., Lange, M., Lomuscio, A. (eds.) 22nd International Symposium on Temporal Representation and Reasoning, TIME 2015, Kassel, Germany, pp. 101-110. IEEE (2015) · Zbl 1423.68288
[16] Kupferman, O., Sattler, U., Vardi, M.Y.: The complexity of the graded \[\mu\] μ-calculus. In: Voronkov, A. (ed.) 18th International Conference on Automated Deduction (CADE) Copenhagen, Denmark, pp. 423-437. Springer (2002) · Zbl 1072.03014
[17] Laroussinie, F.: About the expressive power of CTL combinators. IPL 54(6), 343-345 (1995) · Zbl 0875.68632 · doi:10.1016/0020-0190(95)00053-F
[18] Meier, A.: On the complexity of modal logic variants and their fragments. Ph.D. thesis, Leibniz Universität Hannover, Institut für Theoretische Informatik (2011)
[19] Meier, A., Müller, J.S., Mundhenk, M., Vollmer, H.: Complexity of model checking for logics over Kripke models. Bull. EATCS 108, 50-89 (2012) · Zbl 1394.68233
[20] Meier, A., Mundhenk, M., Thomas, M., Vollmer, H.: The complexity of satisfiability for fragments of CTL and \[\text{ CTL }^*\] CTL∗. IJFCS 20(05), 901-918 (2009) · Zbl 1186.68212
[21] Meier, A., Mundhenk, M., Thomas, M., Vollmer, H.: Erratum: The complexity of satisfiability for fragments of CTL and \[{\text{ CTL }}^*\] CTL∗. Int. J. Found. Comput. Sci. 26(8), 1189 (2015). https://doi.org/10.1142/S012905411592001X · Zbl 1405.68130 · doi:10.1142/S012905411592001X
[22] Mundhenk, M., Weiß, F.: The complexity of model checking for intuitionistic logics and their modal companions. In: Proceedings of RP’10, LNCS, vol. 6227, pp. 146-160. Springer (2010) · Zbl 1287.68110
[23] Mundhenk, M., Weiß, F.: An AC \[^11\]-complete model checking problem for intuitionistic logic. Comput. Complex. 23(4), 637-669 (2014) · Zbl 1522.68336 · doi:10.1007/s00037-013-0062-z
[24] Papadimitriou, C.H.: Computational Complexity. Addison-Wesley, Reading (1994) · Zbl 0833.68049
[25] Pnueli, A.: The temporal logic of programs. In: Proceedings of 18th FOCS, pp. 46-57. IEEE Computer Society Press (1977)
[26] Post, E.: The two-valued iterative systems of mathematical logic. Ann. Math. Stud. 5, 1-122 (1941)
[27] Pratt, V.R.: A near-optimal method for reasoning about action. JCSS 20(2), 231-254 (1980) · Zbl 0424.03010
[28] Prior, A.N.: Time and Modality. Clarendon Press, Oxford (1957) · Zbl 0079.00606
[29] Prior, A.N.: Past, Present, and Future. Clarendon Press, Oxford (1967) · Zbl 0169.29802 · doi:10.1093/acprof:oso/9780198243113.001.0001
[30] Schnoebelen, P.: The complexity of temporal logic model checking. In: AiML, pp. 393-436. King’s College Publications (2002) · Zbl 1084.03013
[31] Vardi, M.Y., Stockmeyer, L.: Improved upper and lower bounds for modal logics of programs: preliminary report. In: STOC ’85, LNCS, pp. 240-251 (1985)
[32] Vardi, M.Y., Stockmeyer, L.: Lower bound in full (2EXPTIME-hardness for \[\text{ CTL }^*\] CTL∗-SAT). http://www.cs.rice.edu/ vardi/papers/ctl_star_lower_bound.pdf (1985). Accessed 31 July 2018
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.