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

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

Реляционная версия многоагентной логики деревьев вычислений 𝒞𝒯ℒ𝒦

Автор(ы)
С. И. Башмаков1, К. А. Смелых1

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

Аннотация
Рассматривается многоагентная логика деревьев вычислений — 𝒞𝒯 ℒ𝒦 (Computation Tree Logic with Knowledge). Каждый агент представляет свой собственный вычислительный маршрут исходной задачи, а каждое новое ветвление возможных вычислительных маршрутов порождает новых агентов. Логика 𝒞𝒯 ℒ𝒦 представляет собой естественное обогащение языка 𝒞𝒯 ℒ дополнительными операторами знания. Предложена реляционная — альтернативная автоматной — семантика логики, описаны свойства 𝒞𝒯 ℒ𝒦𝑅𝑒𝑙-фреймов, доказана финитная аппроксимируемость.
Об авторах

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

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

Ссылка для цитирования
Башмаков С. И., Смелых К. А. Реляционная версия многоагентной логики деревьев вычислений 𝒞𝒯 ℒ𝒦 // Известия Иркутского государственного университета. Серия Математика. 2024. Т. 47. C. 78–92. https://doi.org/10.26516/1997-7670.2024.47.78
Ключевые слова
многоагентная логика, ветвящаяся временная логика, реляционная семантика Крипке, метод фильтрации, финитная аппроксимируемость
УДК
510.643
MSC
03B44, 03B42, 03A05, 03B45, 03B70
DOI
https://doi.org/10.26516/1997-7670.2024.47.78
Литература
  1. Витяев Е. Е. Семантический вероятностный вывод предсказаний // Известия Иркутского государственного университета. Серия Математика. 2017. Т. 21. С. 33–50. https://doi.org/10.26516/1997-7670.2017.21.33
  2. Карпов Ю. Г. Model Checking. Верификация параллельных и распределенных программных систем. СПб. : БХВ-Петербург, 2010. 560 c.
  3. Манцивода А. В., Пономарев Д. К. К семантическому документному моделированию бизнес-процессов // Известия Иркутского государственного университета. Серия Математика. 2019. Т. 29. С. 52–67. https://doi.org/10.26516/1997-7670.2019.29.52
  4. Kripke-style models for logics of evidence and truth / H. Antunes, W. Carnielli, A. Kapsner, A. Rodrigues // Axioms. 2020. Vol. 9, N 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, N 3. P. 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, N 2. P. 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. 1982. Vol. 131. P. 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. P. 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 mknowledge, perfect recall and past: axiomatisation and model-checking // Journal of Applied Non-Classical Logics. 2011. Vol. 21, N 1. P. 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, N 1. P. 195–237.

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