Dynamic temporal logical operations in multi-agent logics

V. V. Rybakov

Algebra i logika, Tome 61 (2022) no. 5, pp. 600-618.

Résumé

We study temporal multi-agent logics using a new approach to defining time for individual agents. It is assumed that in any time state each agent (in a sense) generates its own future time, which will only be available for analysis in the future. That is, the defined time interval depends both on the agent and on the initial state where the agent starts to act. It is also assumed that the agent may have intervals of forgotten (lost) time. We investigate problems of unification and problems of computable recognizing admissible inference rules. An algorithm is found for solving these problems based on the construction of a finite computable set of formulas which is a complete set of unifiers. We use the technique of projective formulas developed by S. Ghilardi. It is proved that any unifiable formula is in fact projective and an algorithm is constructed which creates its projective unifier. Thereby we solve the unification problem, and based at this, find the solution to the open problem of computable recognizing admissible inference rules.

Détail

Keywords: temporal logics, multi-agent logics, admissible inference rules, unification problem, solving algorithms.

Bibliographie

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

[2] 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

[3] D. M. Gabbay, I. Hodkinson, “Temporal logic in the context of databases”, Logic and reality: essays on the legacy of Arthur Prior, Including papers from the Arthur Prior memorial conference (Univ. Canterbury, Christchurch, New Zealand, 1989), ed. B. J. Copeland, Clarendon Press, Oxford, 1996, 69–87 | MR | Zbl

[4] Z. Manna, A. Pnueli, The temporal logic of reactive and concurrent systems. Specification, Springer-Verlag, Berlin etc., 1991 | MR | Zbl

[5] E. A. Emerson, J. Y. Halpern, “Decision procedures and expressiveness in the temporal logic of branching time”, J. Comput. Syst. Sci., 30 (1985), 1–24 | DOI | MR | Zbl

[6] E. M. Clarke, E. A. Emerson, A. P. Sistla, “Automatic verification of finite-state concurrent systems using temporal logic specifications”, ACM Trans. Program. Lang. Syst., 8:2 (1986), 244–263 | DOI | Zbl

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

[8] V. V. Rybakov, “Intranzitivnye vremennye mnogoagentnye logiki, informatsiya i znanie, razreshimost”, Sib. matem. zh., 58:5 (2017), 1128–1143 | MR | Zbl

[9] V. V. Rybakov, “Multi-agent logic's modelling non-monotonic information and reasoning”, Procedia Comput. Sci., 176 (2020), 670–674 | DOI

[10] G. Weiss (ed.), Multiagent systems: A modern approach to distributed artificial intelligence, MIT Press, Cambridge, MA, 1999

[11] M. Wooldridge, An introduction to multiagent systems, J. Wiley Sons Ltd, 2002

[12] R. Fagin, J. Y. Halpern, Y. Moses, M. Y. Vardi, Reasoning about knowledge, MIT Press, Cambridge, MA, 1995 | MR | Zbl

[13] J. A. Robinson, “A machine-oriented logic based on the resolution principle”, J. Assoc. Comput. Mach., 12:1 (1965), 23–41 | DOI | MR | Zbl

[14] D. E. Knuth, P. B. Bendix, “Simple word problems in universal algebras”, Computational problems in abstract algebra, Proc. Conf. (Oxford, 1967), ed. J. Leech, Pergamon Press, Oxford a. o., 1970, 263–297 | MR

[15] F. Baader, W. Snyder, “Unification theory”, Handbook of Automated Reasoning, v. I, eds. A. Robinson et al., North-Holland/Elsevier, Amsterdam, 2001, 447–533

[16] V. V. Rybakov, “Problems of substitution and admissibility in the modal system Grz and in intuitionistic propositional calculus”, Ann. Pure Appl. Logic, 50:1 (1990), 71–106 | DOI | MR | Zbl

[17] V. V. Rybakov, “Rules of inference with parameters for intuitionistic logic”, J. Symb. Log., 57:3 (1992), 912–923 | DOI | MR | Zbl

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

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

[20] S. Ghilardi, “Best solving modal equations”, Ann. Pure Appl. Logic, 102:3 (2000), 183–198 | DOI | MR | Zbl

[21] W. Dzik, P. Wojtylak, “Projective unification in modal logic”, Log. J. IGPL, 20:1 (2012), 121–153 | DOI | MR | Zbl

[22] A. Wrónski, “Transparent verifiers in intermediate logics”, Abstracts 54-th Conf. History Math. (Krakøw, 2008)

[23] V. Rybakov, “Projective formulas and unification in linear temporal logic ${\rm LTL}_U$”, Log. J. IGPL, 22:4 (2014), 665–672 | DOI | MR | Zbl

[24] S. Babenyshev, V. Rybakov, “Linear temporal logic LTL: basis for admissible rules”, J. Log. Comput., 21:2 (2011), 157–177 | DOI | MR | Zbl

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