Список выпусков > Серия «Математика». 2024. Том 47
Реляционная версия многоагентной логики
деревьев вычислений 𝒞𝒯ℒ𝒦
Автор(ы)
С. И. Башмаков1
,
К. А. Смелых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
Литература
- Витяев Е. Е. Семантический вероятностный вывод предсказаний // Известия Иркутского государственного университета. Серия Математика. 2017. Т. 21. С. 33–50. https://doi.org/10.26516/1997-7670.2017.21.33
- Карпов Ю. Г. Model Checking. Верификация параллельных и распределенных программных систем. СПб. : БХВ-Петербург, 2010. 560 c.
- Манцивода А. В., Пономарев Д. К. К семантическому документному моделированию бизнес-процессов // Известия Иркутского государственного университета. Серия Математика. 2019. Т. 29. С. 52–67. https://doi.org/10.26516/1997-7670.2019.29.52
- 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
- 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
- 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
- Chagrov A., Zacharyaschev M. Modal Logic. Oxford University Press, 1997. 605 p.
- 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
- 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
- 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.
- 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.