Тип публикации: статья из журнала
Год издания: 2026
Идентификатор DOI: 10.26516/1997-7670.2026.55.94
Ключевые слова: multi-agent logic, branching temporal logic, Kripke relational semantics, decidability, model construction method, многоагентная логика, ветвящаяся временная логика, реляционная семантика Крипке, разрешимость, метод построения модели
Аннотация: Исследуется многоагентная логика деревьев вычислений относительно реляционной семантики возможных миров Крипке: вопросы разрешимости логики, сложности построения моделей, проверки выполнимости, корректности. Для введённой ранее семантики доказано строгое свойство конечной модели, получены полиномиальные оценки размерности минимальнПоказать полностьюых моделей для произвольных формул. Доказана рекурсивная перечислимость конечных фреймов логики, предложен эффективный алгоритм проверки выполнимости формул, позволяющий заключить разрешимость логики. Полученные полиномиальные оценки находятся в рамках теоретических ожиданий, что позволяет воспринимать исследуемую логику эффективным инструментом анализа многоагентных распределённых систем и практического <i>model-checking</i>, рассчитывать на положительное разрешение вопросов унификации и описания допустимости правил вывода. 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 frame-work 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 model-checking, and to count on a positive resolution of issues of unification and description of the admissibility for inference rules.
Журнал: Известия Иркутского государственного университета. Серия: Математика
Выпуск журнала: Т. 55
Номера страниц: 94-109
ISSN журнала: 19977670
Место издания: Иркутск
Издатель: Иркутский государственный университет