рус 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». 2024. Vol 47

Relational Version of the Multi-agent Computation Tree Logic 𝒞𝒯ℒ𝒦

Author(s)
Stepan I. Bashmakov1, Kirill A. Smelykh1

1Siberian Federal University, Krasnoyarsk, Russian Federation

Abstract
This paper deals with multi-agent computation tree logic — 𝒞𝒯 ℒ𝒦 (Computation Tree Logic with Knowledge). Each agent represents its own computational route of the initial problem, and new branches of possible computational routes spawn new agents. The logic 𝒞𝒯 ℒ𝒦 is a natural enrichment of 𝒞𝒯 ℒ by new knowledge operators. We introduce alternative to automata Kripke’s relational semantics, describes properties of 𝒞𝒯 ℒ𝒦𝑅𝑒𝑙-frame and proves finite approximability
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. Relational Version of the Multi-agent Computation Tree Logic 𝒞𝒯 ℒ𝒦. The Bulletin of Irkutsk State University. Series Mathematics, 2024, vol. 47, pp. 78–92. (in Russian) https://doi.org/10.26516/1997-7670.2024.47.78
Keywords
multi-agent logic, branching temporal logic, Kripke relational semantics, filtration method, finite approximability
UDC
510.643
MSC
03B44, 03B42, 03A05, 03B45, 03B70
DOI
https://doi.org/10.26516/1997-7670.2024.47.78
References
  1. Vityaev E.E. Semantic probabilistic inference of predictions. The Bulletin of Irkutsk State University. Series Mathematics, 2017, vol. 21, pp. 33–50. https://doi.org/10.26516/1997-7670.2017.21.33
  2. Karpov Yu.G. Model checking. Verification of parallel and distributed program systems. St. Petersburg, BHV-St. Petersburg Publ., 2010, 560 p.
  3. Mantsivoda A.V., Ponomaryov D.K. Towards Semantic Document Modelling of Business Processes. The Bulletin of Irkutsk State University. Series Mathematics, 2019, vol. 29, pp. 52–67. https://doi.org/10.26516/1997-7670.2019.29.52
  4. Antunes H., Carnielli W., Kapsner A., Rodrigues A. Kripke-style models for logics of evidence and truth. Axioms, 2020, vol. 9, no. 3: 100. https://doi.org/10.3390/axioms9030100
  5. Bashmakov S.I., Zvereva T.Yu. Unification and finite model property for linear step-like temporal multi-agent logic with the universal modality. Bulletin of the Section of Logic, 2022, vol. 51, no. 3, pp. 345–361. https://doi.org/10.18778/0138-0680.2022.16
  6. Bashmakov S.I., Zvereva T.Yu. Linear Step-like Logic of Knowledge LTK.sl. Siberian Electronic Mathematical Reports, 2023, vol. 20, no. 2, pp. 1361–1373. https://doi.org/10.33048/semi.2023.20.082
  7. Chagrov A., Zacharyaschev M. Modal Logic. Oxford University Press, 1997, 605 p.
  8. Clarke E.M., Emerson E.A. Design and synthesis of synchronization skeletons using branching time temporal logic. Logics of Programs. Logic of Programs 1981. Lecture Notes in Computer Science, vol. 131, 1982, pp. 52–71. https://doi.org/10.1007/BFb0025774
  9. 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
  10. Guelev D.P., Dima C., Enea C. An alternating-time temporal logic with knowledge, perfect recall and past: axiomatisation and model-checking. Journal of Applied Non-Classical Logics, 2011, vol. 21, no. 1, pp. 93–131. https://doi.org/10.3166/jancl.21.93-131
  11. Halpern J.Y., Vardi M.Y. The complexity of reasoning about knowledge and time. I. Lower bounds. J. Computer and System Sciences, 1989, vol. 38, no. 1, pp. 195–237. https://doi.org/10.1016/0022-0000(89)90039-1

Full text (russian)