Kripke Incompleteness of First-order Calculi with Temporal Modalities of CTL and Near Logics
##plugins.themes.bootstrap3.article.sidebar##
Published:
21.04.2015
##plugins.themes.bootstrap3.article.main##
Abstract
We study an expressive power of temporal operators used in such logics of branching time as computational tree logic or alternating-time temporal logic. To do this we investigate calculi in the first-order language enriched with the temporal operators used in such logics. We show that the resulting languages are so powerful that many ‘natural’ calculi in the languages are not Kripke complete; for example, if a calculus in such language is correct with respect to the class of all serial linear Kripke frames (even just with constant domains) then it is not Kripke complete. Some near questions are discussed.
##plugins.generic.usageStats.downloads##
##plugins.generic.usageStats.noStats##
##plugins.themes.bootstrap3.article.details##
How to Cite
Kotikova E. A., Rybakov M. N. Kripke Incompleteness of First-order Calculi with Temporal Modalities of CTL and Near Logics // Logicheskie Issledovaniya / Logical Investigations. 2015. VOL. 21. № 1. C. 86-99.
Issue
Section
Papers
References
Karpov, Yu.G. Model checking: Verifikatsiya parallel’nykh i raspredelennykh programmnykh sistem [Model checking: Verification of parallel and distributed software systems]. Sankt-Peterburg: BKhV-Peterburg, 2010. 560 pp. (In Russian)
Mal’tsev, A.I. Algoritmy i rekursivnye funktsii [Algorithms and recursive functions]. M.: Nauka, Fizmatlit, 1986. 367 pp. (In Russian)
Maslov, Yu. S., Mints E. S., Orevkov V. P. “Nerazreshimost’ v konstruktivnom ischislenie predikatov nekotorykh klassov i formul, soderzhashchikh tol’ko odnomestnye predikatnye peremennye” [Unsolvability in constructive predicate calculus certain classes of formulas containing only single predicate variables], Doklady AN SSSR [Reports of the Academy of Sciences USSR], 1965, vol. 163, no 2, pp. 295–297. (In Russian)
Rybakov, M.N. “Ob algoritmicheskoi vyrazitel’nosti modal’nogo yazyka s odnoi lish’ odnomestnoi predikatnoi bukvoi” [About algorithmic expressiveness modal language with only one single predicate letter], Logicheskie issledovaniya [Logical investigations]. M.: Nauka, 2002, vol.9, pp. 179–201. (In Russian)
Rybakov, M.N., Chagrov, A.V. “Standartnye perevody neklassicheskikh formul i otnositel’naya razreshimost’ logik” [Standard formulas and transfers of nonclassical logics relative solvability], Trudy nauchno-issledovatel’skogo seminara Logicheskogo tsentra Instituta Filosofii RAN [Proceedings of the Research Seminar Logic Center Institute of Philosophy RAS]. M.: Izdatel’stvo Instituta Filosofii RAN, 2000, vol. XIV, pp. 81–98. (In Russian)
Trakhtenbrot, B.A. “Nevozmozhnost’ algoritma dlya problemy razreshimosti na konechnykh klassakh” [The impossibility of an algorithm for the solvability of the problem in the final classes], Doklady Akademii Nauk SSSR [Reports of the Academy of Sciences USSR], 1950, vol. 70, no 4, pp. 596–572. (In Russian)
Alur, R., Henzinger, T.A., Kupferman, O. “Alternating-time temporal logic”, Journal of the ACM, 2002, vol. 19, no 5, pp. 672–713.
Boolos, G.S., Burgess, J.P., Jeffrey, R.C. Computability and Logic. Cambridge: Cambridge University Press, 2007. 366 pp.
Clarke, E.M., Grumberg, O., Peled, D.A. Model Checking. Cambridge: The MIT Press, 1999. 314 pp.
Craig, W. “On axiomatizability within a system”, The Journal of Symbolic Logic, 1953, vol. 18, no 1, pp. 30–32.
Emerson, E.A., Halpern, J.Y. “Decision procedures and expressiveness in the temporal logic of branching time”, Journal of Computer and System Sciences, 1985, no 30(1), pp. 1–24.
Emerson, E.A., Julta, C.S. “The complexity of tree automata and logics of programs”, In Proceedings of the 29th Annual Symposium on Foundations of Computer Science, 1988, pp. 328—337.
Kleene, S.C. Mathematical Logic. John Wiley & Sons, Inc: New York, London, Sydney, 1967. 432 pp.
Konchakov, R., Kurucz, A., Zakharyaschev, M. “Undecidability of first-order intuitionistic and modal logics with two variables”, Bulletin of Symbolic Logic, 2011, vol. 11, pp. 428–438.
Kotikova, E.A., Rybakov M.N. “First-Order Logics of Branching Time: On Expressive Power of Temporal Operators”, Logical Investigations, 2013, vol. 19, pp. 68–99.
Kripke, S. “The Undecidability of Monadic Modal Quantificational Theory”, Zeitschrift f_ur Mathematische Logik und Grundlagen der Mathematik, 1962, vol. 8, pp. 113–116.
Laroussinie, F. “About the expressive power of CTL combinators”, Information Processing Letters, 1995, no 54(6), pp. 343–345.
Prior, A.N. Past, present and future. Oxford: Oxford University press, 1967. 228 pp.
Schewe, S. “$ATL^{*}$ satisfiability is 2EXPTIME-complete”, in: Automata, Languages, and Programming, ed. by L. Aceto et al. 2008, vol. 5126 of Lecture Notes in Computer Science, pp. 373–385.
Shoenfield, J.R. Degrees of Unsolvability. North-Holland Publishing Company: American Elsevier Publishing Company, 1971.
Sistla, A.P., Clarke, E.M. “The Complexity of Propositional Linear Temporal Logics”, Journal of the Association for Computing Machinery, 1985 (July), vol. 32, no 3, pp. 733–749.
Skvortsov, D. “On The Predicate Logics of Finite Kripke Frames”, Studia Logica, 1995, vol. 54, pp. 79–88.
Vardi, M.Y., Stockmeyer, L. “Improved upper and lower bounds for modal logics of programs: Preliminary report”, In Proceedings of the seventeenth annual ACM symposium on Theory of computing, 1985, pp. 240—252.
Walther D., Lutz C., Walter F., Wooldridge M. “ATL satisfiability is indeed EXPTIME-complete”, Journal of Logic and Computation, 2006, no 16(6), pp. 765–787.
Mal’tsev, A.I. Algoritmy i rekursivnye funktsii [Algorithms and recursive functions]. M.: Nauka, Fizmatlit, 1986. 367 pp. (In Russian)
Maslov, Yu. S., Mints E. S., Orevkov V. P. “Nerazreshimost’ v konstruktivnom ischislenie predikatov nekotorykh klassov i formul, soderzhashchikh tol’ko odnomestnye predikatnye peremennye” [Unsolvability in constructive predicate calculus certain classes of formulas containing only single predicate variables], Doklady AN SSSR [Reports of the Academy of Sciences USSR], 1965, vol. 163, no 2, pp. 295–297. (In Russian)
Rybakov, M.N. “Ob algoritmicheskoi vyrazitel’nosti modal’nogo yazyka s odnoi lish’ odnomestnoi predikatnoi bukvoi” [About algorithmic expressiveness modal language with only one single predicate letter], Logicheskie issledovaniya [Logical investigations]. M.: Nauka, 2002, vol.9, pp. 179–201. (In Russian)
Rybakov, M.N., Chagrov, A.V. “Standartnye perevody neklassicheskikh formul i otnositel’naya razreshimost’ logik” [Standard formulas and transfers of nonclassical logics relative solvability], Trudy nauchno-issledovatel’skogo seminara Logicheskogo tsentra Instituta Filosofii RAN [Proceedings of the Research Seminar Logic Center Institute of Philosophy RAS]. M.: Izdatel’stvo Instituta Filosofii RAN, 2000, vol. XIV, pp. 81–98. (In Russian)
Trakhtenbrot, B.A. “Nevozmozhnost’ algoritma dlya problemy razreshimosti na konechnykh klassakh” [The impossibility of an algorithm for the solvability of the problem in the final classes], Doklady Akademii Nauk SSSR [Reports of the Academy of Sciences USSR], 1950, vol. 70, no 4, pp. 596–572. (In Russian)
Alur, R., Henzinger, T.A., Kupferman, O. “Alternating-time temporal logic”, Journal of the ACM, 2002, vol. 19, no 5, pp. 672–713.
Boolos, G.S., Burgess, J.P., Jeffrey, R.C. Computability and Logic. Cambridge: Cambridge University Press, 2007. 366 pp.
Clarke, E.M., Grumberg, O., Peled, D.A. Model Checking. Cambridge: The MIT Press, 1999. 314 pp.
Craig, W. “On axiomatizability within a system”, The Journal of Symbolic Logic, 1953, vol. 18, no 1, pp. 30–32.
Emerson, E.A., Halpern, J.Y. “Decision procedures and expressiveness in the temporal logic of branching time”, Journal of Computer and System Sciences, 1985, no 30(1), pp. 1–24.
Emerson, E.A., Julta, C.S. “The complexity of tree automata and logics of programs”, In Proceedings of the 29th Annual Symposium on Foundations of Computer Science, 1988, pp. 328—337.
Kleene, S.C. Mathematical Logic. John Wiley & Sons, Inc: New York, London, Sydney, 1967. 432 pp.
Konchakov, R., Kurucz, A., Zakharyaschev, M. “Undecidability of first-order intuitionistic and modal logics with two variables”, Bulletin of Symbolic Logic, 2011, vol. 11, pp. 428–438.
Kotikova, E.A., Rybakov M.N. “First-Order Logics of Branching Time: On Expressive Power of Temporal Operators”, Logical Investigations, 2013, vol. 19, pp. 68–99.
Kripke, S. “The Undecidability of Monadic Modal Quantificational Theory”, Zeitschrift f_ur Mathematische Logik und Grundlagen der Mathematik, 1962, vol. 8, pp. 113–116.
Laroussinie, F. “About the expressive power of CTL combinators”, Information Processing Letters, 1995, no 54(6), pp. 343–345.
Prior, A.N. Past, present and future. Oxford: Oxford University press, 1967. 228 pp.
Schewe, S. “$ATL^{*}$ satisfiability is 2EXPTIME-complete”, in: Automata, Languages, and Programming, ed. by L. Aceto et al. 2008, vol. 5126 of Lecture Notes in Computer Science, pp. 373–385.
Shoenfield, J.R. Degrees of Unsolvability. North-Holland Publishing Company: American Elsevier Publishing Company, 1971.
Sistla, A.P., Clarke, E.M. “The Complexity of Propositional Linear Temporal Logics”, Journal of the Association for Computing Machinery, 1985 (July), vol. 32, no 3, pp. 733–749.
Skvortsov, D. “On The Predicate Logics of Finite Kripke Frames”, Studia Logica, 1995, vol. 54, pp. 79–88.
Vardi, M.Y., Stockmeyer, L. “Improved upper and lower bounds for modal logics of programs: Preliminary report”, In Proceedings of the seventeenth annual ACM symposium on Theory of computing, 1985, pp. 240—252.
Walther D., Lutz C., Walter F., Wooldridge M. “ATL satisfiability is indeed EXPTIME-complete”, Journal of Logic and Computation, 2006, no 16(6), pp. 765–787.