First-order logics of branching time


E.A. Kotikova
M.N. Rybakov


We consider the logic QCTL, a first-order exten- sion of CTL defined as a logic of Kripke frames for CTL. We study the question about recursive enumerability of its fragments specified by a set of temporal modalities we use. Then we discuss some questions concerned axiomatizability and Kripke completeness.






Boolos, G.S., Burgess, J.P., and R.C. Jeffrey, Computability and Logic, Cambridge University Press, 2007.
Clarke, E.M., Grumberg, O., and D.A. Peled, Model Cheking, The MIT Press, 1999.
Gabbay, D., Shehtman, V., and D. Skvortsov, Quantification in Nonclassical Logic. Preliminary draft.
Hodkinson, I., and M. Reynolds, Temporal Logic, in P. Blackburn, J. Van Benthem and F. Wolter (eds.), Handbook of Modal Logic, Elsevier, 2007, pp. 655–720.
Hodkinson, I., Wolter, F., and M. Zakharyaschev, Decidable fragments of first-order temporal logics, Annals of Pure and Apllied Logic 106:85–134, 2000.
Hodkinson, I., Wolter, F., and M. Zakharyaschev, Decidable and undecidable fragments of first-order branching temporal logics, Proceedings of the 17th Annual IEEE Symposium on Logic in Computer Science, LICS, 2002, pp. 393–402.
Kontchakov, R., Kurucz, A., and M. Zakharyaschev, Undecidability of First-Order Intuitionistic and Modal Logics with Two Variables, Bulletin of Symbolic Logic 11(3):428–438, 2005.
Kripke, S.A., The Undecidability of Monadic Modal Quantification Theory, Zeitschrift f_ur mathematische Logik und Grundlagen der Mathematik 8:113–116, 1962.
Nerode, A., and R. Shore, Second Order Logic and First Order Theories of Reducibility Orderings, in J. Barwise, H.J. Keisler, K. Kuner (eds.), The Kleene Symposium, North-Holland, Amsterdam, 1980, pp. 181–200.
Prior, A.N., Past, present and future, Oxford University press, 1967.
Trakhtenbrot, B.A., The Impossibility of an Algorithm for the Decidability Problem on Finite Classes, Proceedings of the USSR Academy of Sciences 70(4):569–572, 1950. (in Russian)
Wolter, F., and M. Zakharyaschev, Decidable fragments of firstorder modal logics, Journal of Symbolic Logic 66:1415–1438, 2001.