Temporal logic with overlap temporal relations generated by time states themselves

V. V. Rybakov

Sibirskie èlektronnye matematičeskie izvestiâ, Tome 17 (2020), pp. 923-932.

Résumé

We study a temporal logic with non–standard temporal accessibility relations. This logic is generated by semantic underground models, and any such a model has a base formed by a frame with temporal relations generated by temporal states themselves; potentially, any state possesses its own temporal accessibility relation, and it is possible that all of them can be different. We consider this to be the most plausible modelling, because any time state has, in principle, its own view on what is past (or future). Time relations may have non–empty overlaps and they can be totally intransitive. Thus, this approach may be suitable for analysis of the most general cases of reasoning about computation, information flows, reliability, and other areas of AI and CS. The main mathematical question under consideration here is the existence of algorithms for solving satisfiability problems. Here we solve this problem and find the required algorithms. In the final part of our paper we formulate some interesting open problems.

Détail

Keywords: temporal logic, non–classical logics, knowledge representation, deciding algorithms, computability, satisfiability, decidability.
Mots-clés : information, information

Bibliographie

[1] F. Baader, P. Marantidis, A. Mottet, A. Okhotin, “Extensions of unificationmodulo ACUI”, Mathematical Structures in Computer Science, 2019, 1–30 | MR

[2] F. Baader, P. Narendran, UNIF-97, Proceedings of the 11th International Workshop on Unification, LIFO Technical Report 97-8, 1997 | MR | Zbl

[3] S.Babenyshev, V. Rybakov, “Linear Temporal Logic LTL: Basis for Admissible Rules”, J. Log. Comput., 21:2 (2011), 157–177 | DOI | MR | Zbl

[4] H. Friedman, “One Hundred and Two Problems in Mathematical Logic”, J. Symb. Log., 40 (1975), 113–129 | DOI | MR | Zbl

[5] D.M. Gabbay, I.M. Hodkinson, “An axiomatization of the temporal logic with until and since over the real numbers”, J. Log. Comput., 1:2 (1990), 229–259 | DOI | MR | Zbl

[6] D.M. Gabbay, I.M. Hodkinson, M.A. Reynolds, Temporal Logic, v. 1, Mathematical foundations and computational aspects, Clarendon Press, Oxford, 1994 | MR | Zbl

[7] R. Goldblatt, “Logics of Time and Computations”, Chapter 6, CSLI Lecture Notes, 7, 1992 | MR

[8] V. Goranko, “Hierarchies of Modal and Temporal Logics with Reference Pointers”, J. Log. Lang. Inf., 5:1 (1996), 1–24 | DOI | MR | Zbl

[9] S. Ghilardi, “Unification in Intuitionistic Logic”, J. Symb. Log., 64:2 (1999), 859–880 | DOI | MR | Zbl

[10] S. Ghilardi, “Unification Through Projectivity”, J. Log. Comput., 7:6 (1997), 733–752 | DOI | MR | Zbl

[11] S. Odintsov, V. Rybakov, “Inference Rules in Nelson's Logics, Admissibility and Weak Admissibility”, Log. Univers., 9:1 (2015), 93–120 | DOI | MR | Zbl

[12] S. Odintsov, V. Rybakov, “Unification and admissible rules for paraconsistent minimal Johanssons' logic J and positive intuitionistic logic $IPC^+$”, Ann. Pure Appl. Logic, 164:7–8 (2013), 771–784 | DOI | MR | Zbl

[13] V.Rybakov, “Refined common knowledge logics or logics of common information”, Arch. Math. Log., 42:2 (2003), 179–200 | DOI | MR | Zbl

[14] V. Rybakov, “Logical Consecutions in Discrete Linear Temporal Logic”, J. Symb. Log., 70:4 (2005), 1137–1149 | DOI | MR | Zbl

[15] V. Rybakov, “Linear temporal logic with until and next, logical consecutions”, Ann. Pure Appl. Logic, 155:1 (2008), 32–45 | DOI | MR | Zbl

[16] V. Rybakov, “Logic of knowledge and discovery via interacting agents-Decision algorithm for true and satisfiable statements”, Inf. Sci., 179:11 (2009), 1608–1614 | DOI | MR | Zbl

[17] V. Rybakov, “Linear Temporal Logic $LTL_{K}$ extended by Multi-Agent Logic $K_n$ with Interacting Agents”, J. Log. Comput., 19:6 (2009), 989–1017 | DOI | MR | Zbl

[18] V. Rybakov, “Logical Analysis for Chance Discovery in Multi-Agents' Environment”, Conference Proceedings, KES 2012, Springer, 2012, 1593–1601

[19] V. Rybakov, “Writing out unifiers in linear temporal logic”, J. Log. Comput., 22:5 (2012), 1199–1206 | DOI | MR | Zbl

[20] V.Rybakov, “Non-transitive linear temporal logic and logical knowledge operations”, J. Log. Comput., 26:3 (2016), 945–958 | DOI | MR | Zbl

[21] V.V. Rybakov, “Nontransitive temporal multiagent logic, information and knowledge, deciding algorithms”, Sib. Math. J., 58:5 (2017), 875–886 | DOI | MR | Zbl

[22] V. Rybakov, “Multiagent temporal logics with multivaluations”, Sib. Math. J., 59:4 (2018), 710–720 | DOI | MR | Zbl

[23] V. Rybakov, “Linear Temporal Logic with Non-transitive Time, Algorithms for Decidability and Verification of Admissibility”, Outstanding Contributions to Logic, Springer, 2018, 219–243 | DOI | MR | Zbl

[24] V. Rybakov, “Temporal multi-valued logic with lost worlds in the past”, Sib. Electron. Math. Izv., 15 (2018), 436–449 | MR | Zbl

[25] V. Rybakov, “Branching time agents' logic, satisfiability problem by rules in reduced form”, Sib. Electron. Math. Izv., 16 (2019), 1158–1170 | DOI | MR | Zbl

[26] R. Schmidt, D. Tishkovsky, “Solving rule admissibility problem for S4 by a tableau method”, Automated Reasoning Workshop, 2011, 30

[27] S. Babenyshev, V. Rybakov, R. Schmidt, D. Tishkovsky, “A tableau method for checking rule admissibility in S4”, Electronic Notes in Theoretical Computer Science, 262 (2010), 17–32 | DOI | MR | Zbl

[28] J. van Benthem, “Tense logic and time”, Notre Dame J. Formal Logic, 25:1 (1984), 1–16 | DOI | MR | Zbl

[29] M. Vardi, “An automata-theoretic approach to linear temporal logic”, Y. Banff Higher Order Workshop, 1995, 238–266 http://citeseer.ist.psu.edu/vardi96automatatheoretic.html

[30] M. Vardi, “Reasoning about the past with two-way automata”, ICALP, LNCS, 1443, eds. Larsen K. G. et al., 1998, 628–641 | MR | Zbl

[31] Yde Venema, “Temporal Logic”, The Blackwell Guide on Philosophical Logic, ed. Lou Goble, Blackwell Publishers, Oxford, 2001, 203–223 | MR | Zbl