рус eng
«THE BULLETIN OF IRKUTSK STATE UNIVERSITY». SERIES «MATHEMATICS»
«IZVESTIYA IRKUTSKOGO GOSUDARSTVENNOGO UNIVERSITETA». SERIYA «MATEMATIKA»
ISSN 1997-7670 (Print)
ISSN 2541-8785 (Online)

List of issues > Series «Mathematics». 2026. Vol 55

Decidability of Multi-agent Logic of Computation Trees 𝒞𝒯 ℒ𝒦𝑅𝑒𝑙

Author(s)

Stepan I. Bashmakov , Kirill A. Smelykh

Siberian Federal University, Krasnoyarsk, Russian Federation 

Abstract
We continue to explore the multi-agent logic of computational trees relative to the relational Kripke semantics of possible worlds: we investigate the question of logical solvability, the complexity of model construction, feasibility testing, and correctness. For the semantics introduced earlier, we proved a strong finite model property, and obtained polynomial estimates of the dimension of minimal models for an arbitrary formulas. We proved the recursive enumerability of finite frames of logic and proposed an effective algorithm for checking the feasibility of formulas, which makes it possible to conclude the solvability of logic. The obtained polynomial estimates are within the framework of theoretical expectations, which makes it possible to perceive the logic under study as an effective tool for analyzing multi-agent distributed systems and practical modelchecking, and to count on a positive resolution of issues of unification and description of the admissibility for inference rules.
About the Authors

Stepan I. Bashmakov, Cand. Sci. (Phys.-Math.), Assoc. Prof., Siberian Federal University, Krasnoyarsk, 660041, Russian Federation, krauder@mail.ru

Kirill A. Smelykh, Student, Siberian Federal University, Krasnoyarsk, 660041, Russian Federation, lastth@yandex.ru

For citation
Bashmakov S. I., Smelykh K. A. Decidability of Multi-agent Logic of Computation Trees 𝒞𝒯 ℒ𝒦𝑅𝑒𝑙. The Bulletin of Irkutsk State University. Series Mathematics, 2026, vol. 55, pp. 94–109. (in Russian) https://doi.org/10.26516/1997-7670.2026.55.94
Keywords
multi-agent logic, branching temporal logic, Kripke relational semantics, decidability, model construction method
UDC
510.643
MSC
03B44, 03B42, 03A05, 03B45, 03B70
DOI
https://doi.org/10.26516/1997-7670.2026.55.94
References
  1. Bashmakov S.I., Smelykh K. A Relational version of the multi-agent computation tree logic CTLK. The Bulletin of Irkutsk State University. Series Mathematics, 2024, vol. 47, pp. 78–92. https://doi.org/10.26516/1997-7670.2024.47.78
  2. Baier C., Katoen J.P. MIT press, 2008.
  3. Blackburn P., De Rijke M., Venema Y. Modal logic. Cambridge Univ. Press, 2001, vol. 53, 554 p.
  4. Calegari R. et al. Logic-based technologies for multi-agent systems: a systematic literature review Autonomous Agents and Multi-Agent Systems, 2021, vol. 35, no. 1, p. 1.
  5. Chagrov A., Zacharyaschev M. Modal Logic, Oxford Univ. Press, 1997, 605 p.
  6. Darwiche A. A logical approach to factoring belief networks. Proceedings of the 8ts Internat. Conference on Principles of Knowledge Representation and Reasoning, 2002, vol. 2, pp. 409–420.
  7. Dima C. Revisiting satisfiability and model-checking for CTLK with synchrony and perfect recall. Computational Logic in Multi-Agent Systems. CLIMA 2008. Lecture Notes in Computer Science, 2008, vol. 5405, pp. 117–131. https://doi.org/10.1007/978-3-642-02734-5_8
  8. Emerson E.A., Halpern J.Y. Decision procedures and expressiveness in the temporal logic of branching time. Proceedings of 14th annual ACM symposium on Theory of computing, 1982, pp. 169–180.
  9. He L., Liu G., Zhou M. Petri-net-based model checking for privacy-critical multiagent systems. Transactions on Computat. Social Systems, 2022, vol. 10, no. 2, pp. 563–576.
  10. Lim´on Y., B´arcenas E., Ben´ıtez-Guerrero E Depth-first reasoning on trees. Computaci´on y Sistemas, 2018, vol. 22, no. 1, pp. 189–201.
  11. Srinivasan M., Coogan S., Egerstedt M. Control of multi-agent systems with finite time control barrier certificates and temporal logic 2018 IEEE Conference on Decision and Control (CDC). IEEE, 2018, pp. 1991–1996.

Full text (russian)