×

Axiomatization of a branching time logic with indistinguishability relations. (English) Zbl 1392.03027

Summary: Trees with indistinguishability relations provide a semantics for a temporal language “composed by” the Peircean tense operators and the Ockhamist modal operator. In this paper, a finite axiomatization with a non standard rule for this language interpreted over bundled trees with indistinguishability relations is given. This axiomatization is proved to be sound and strongly complete.

MSC:

03B44 Temporal logic
PDFBibTeX XMLCite
Full Text: DOI

References:

[1] Ben-Ari, M., Manna, Z., & Pnueli, A. (1983). The temporal logic of branching time. Acta Informatica, 20.3, 207-226. · Zbl 0533.68036 · doi:10.1007/BF01257083
[2] Burgess, J. (1980). Decidability for branching time. Studia Logica, 39.2, 203-218. · Zbl 0467.03006 · doi:10.1007/BF00370320
[3] Belnap, N., Perloff, M., & Xu, M. (2001). Facing the future. Agents and choices in our indeterminist world. New York: Oxford University Press.
[4] Emerson, E., & Clarke, E. (1982). Using branching time temporal logic to synthesise synchronisation skeletons. Science of Computer Programming, 2.3, 241-266. · Zbl 0514.68032 · doi:10.1016/0167-6423(83)90017-5
[5] Emerson, E., & Halpern, J (1986). ‘Sometimes’ and ‘not never’ revisited: On branching versus linear time. Journal of the ACM, 33.1, 151-178. · Zbl 0629.68020 · doi:10.1145/4904.4999
[6] Gabbay, D. (1981). An irreflexivity lemma with applications to axiomatizations of conditions on tense frames. In Mönich, U. (Ed.) Aspects of philosophical logic (pp. 67-89). Dordrecht: D. Reidel Publishing Company. · Zbl 0519.03008
[7] Gabbay, D., Hodkinson, I., & Reynolds, M. (1994). Temporal logic: Mathematical foundation and computational aspects. Vol. I. London: Oxford University Press. · Zbl 0875.03007 · doi:10.1007/BFb0013976
[8] Kamp, H. (1968). Tense logic and the theory of linear order. PhD thesis. Los Angeles: University of California. · Zbl 1002.03015
[9] Laroussinie, F., & Schnoebelen, P. (1994). A hierarchy of temporal logics with past. In Enjalbert, P., Mayr, E., & Wagner, K. (Eds.) Proceedings of STACS?94, Vol. 775 of Lecture Notes in Computer Science (pp. 47-58). Heidelberg: Springer-Verlag. · Zbl 0873.68068
[10] Nishimura, H. (1979). Is the semantics of branching structures adequate for chronological modal logics?. Journal of Philosophical Logic, 8.1, 469-475. · Zbl 0415.03016
[11] Øhrstrøm, P., & Hasle, P.F.V. (1996). Temporal logic: From ancient ideas to artificial intelligence. Kluver Academic Publishers. · Zbl 0855.03003
[12] A. (1967). Prior, Past, present and future. Clarendon Press. · Zbl 0169.29802
[13] Reynolds, M. (2001). An axiomatization of full computation tree logic. Journal of Symbolic Logic, 66.3, 1011-1057. · Zbl 1002.03015 · doi:10.2307/2695091
[14] Reynolds, M. (2002). Axioms for branching time. Journal of Logic and Computation, 12.4, 679-697. · Zbl 1004.03015 · doi:10.1093/logcom/12.4.679
[15] Reynolds, M. (2002). An axiomatization of Prior’s Ockhamist logic of historical necessity. In Balbiani, P., Suzuki, N., Wolter, F., & Zakharyaschev, M. (Eds.) Advances in Modal Logic, (Vol. 4 pp. 355-370). · Zbl 1082.03015
[16] Reynolds, M. (2005). An axiomatization of PCTL*. Information and Computation, 201.1, 72-119. · Zbl 1099.03013 · doi:10.1016/j.ic.2005.03.005
[17] Stirling, C. (1992). Modal and temporal logics. In Abramsky, S., Gabbay, D., & Maibaum, T. (Eds.) Handbook of Logic in Computer Science Volume 2 (pp. 477-563). Oxford: Clarendon Press.
[18] Thomason, R. (1984). Combinations of tense and modality. In Gabbay, D., & Guenthner, F. (Eds.) Handbook of philosophical logics, Vol II: Extensions of Classical Logic (pp. 135-165). Dordrecht: Kluwer Academic Publisher. · Zbl 0875.03047
[19] Zanardo, A. (1985). A finite axiomatization of the set of strongly valid Ockhamist formulas. Journal of Philosophical Logic, 14.4, 447-468. · Zbl 0579.03015 · doi:10.1007/BF00649485
[20] Zanardo, A. (1990). Axiomatization of ‘Peircean’ branching-time logic. Studia Logica, 49.2, 183-195. · Zbl 0724.03014 · doi:10.1007/BF00935598
[21] Zanardo, A., & Carmo, J. (1993). Ockhamist computational logic: past-sensitive necessitation in CTL. Journal of Logic and Computation, 3.3, 249-268. · Zbl 0801.03016 · doi:10.1093/logcom/3.3.249
[22] Zanardo, A. (1998). Undivided and indistinguishable histories in branching-time logics. Journal of Logic, Language and Information, 7.3, 297-315. · Zbl 0921.03024 · doi:10.1023/A:1008259000544
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.