рус eng
«ИЗВЕСТИЯ ИРКУТСКОГО ГОСУДАРСТВЕННОГО УНИВЕРСИТЕТА». СЕРИЯ «МАТЕМАТИКА»
«IZVESTIYA IRKUTSKOGO GOSUDARSTVENNOGO UNIVERSITETA». SERIYA «MATEMATIKA»
«THE BULLETIN OF IRKUTSK STATE UNIVERSITY». SERIES «MATHEMATICS»
ISSN 1997-7670 (Print)
ISSN 2541-8785 (Online)

Список выпусков > Серия «Математика». 2026. Том 55

Разрешимость многоагентной логики деревьев вычислений 𝒞𝒯 ℒ𝒦𝑅𝑒𝑙

Автор(ы)

С. И. Башмаков , К. А. Смелых

Сибирский федеральный университет, Красноярск, Российская Федерация

Аннотация
Исследуется многоагентная логика деревьев вычислений относительно реляционной семантики возможных миров Крипке: вопросы разрешимости логики, сложности построения моделей, проверки выполнимости, корректности. Для введённой ранее семантики доказано строгое свойство конечной модели, получены полиномиальные оценки размерности минимальных моделей для произвольных формул. Доказана рекурсивная перечислимость конечных фреймов логики, предложен эффективный алгоритм проверки выполнимости формул, позволяющий заключить разрешимость логики. Полученные полиномиальные оценки находятся в рамках теоретических ожиданий, что позволяет воспринимать исследуемую логику эффективным инструментом анализа многоагентных распределённых систем и практического model-checking, рассчитывать на положительное разрешение вопросов унификации и описания допустимости правил вывода.
Об авторах

Башмаков Степан Игоревич, канд. физ.-мат. наук, доц., Сибирский федеральный университет, Красноярск, 660041, Российская Федерация, krauder@mail.ru

Смелых Кирилл Александрович, студент, Сибирский федеральный университет, Красноярск, 660041, Российская Федерация, lastth@yandex.ru

Ссылка для цитирования
Башмаков С. И., Смелых К. А. Разрешимость многоагентной логики деревьев вычислений 𝒞𝒯 ℒ𝒦𝑅𝑒𝑙 // Известия Иркутского государственного университета. Серия Математика. 2026. Т. 55. C. 94–109. https://doi.org/10.26516/1997-7670.2026.55.94
Ключевые слова
многоагентная логика, ветвящаяся временная логика, реляционная семантика Крипке, разрешимость, метод построения модели
УДК
510.643
MSC
03B44, 03B42, 03A05, 03B45, 03B70
DOI
https://doi.org/10.26516/1997-7670.2026.55.94
Литература
  1. Башмаков С. И., Смелых К. А. Реляционная версия многоагентной логики деревьев вычислений CTLK // Известия Иркутского государственного университета. Серия Математика. 2024. Т. 47. С. 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. Logic-based technologies for multi-agent systems: a systematic literature review / R. Calegari [et al.] // Autonomous Agents and Multi-Agent Systems. 2021. Vol. 35, N 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 8th Internat. Conference on Principles of Knowledge Representation and Reasoning. 2002. Vol. 2. P. 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. P. 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 the 14th Annual ACM Symposium on Theory of Computing. 1982. P. 169–180.
  9. He L., Liu G., Zhou M. Petri-net-based model checking for privacy-critical multiagent systems // Transactions on Computational Social Systems. 2022. Vol. 10, N 2. P. 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. N 1. P. 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. С. 1991–1996.

Полная версия (русская)