Тип публикации: статья из журнала
Год издания: 2021
Идентификатор DOI: 10.33048/smzh.2021.62.313
Ключевые слова: temporal logic, multiagent logic, satisfiability problem, deciding algorithm, Временные логики, мультиагентные логики, проблема выполнимости, разрешающие алгоритмы
Аннотация: Изучается временная логика ветвящегося времени с отношениями временной достижимости для агентов, различных по протяженности и содержанию. Найден алгоритм для разрешения проблемы выполнимости и разрешимости самой логики через описание конечных выполняющих моделей вычислимого размера (через размер входных формул). Сняты ограничения нПоказать полностьюа величину всех интервалов временной достижимости для агентов (быть всем внутри общего интервалавременной достижимости для любой локальной точки времени): они могут быть произвольными. Сформулированы некоторые открытые проблемы. Under study are the branching time temporal logics with temporal accessibility relations for the agents different in length and content. We find an algorithm for solving the problems of satisfiability and decidability of the logic through describing finite satisfiable models of computable size (through the size of the input formulas). We remove the constraints on the size of all temporal accessibility intervals for the agents (to be all inside a common temporal accessibility interval at any local time point); i.e., all constraints can be arbitrary. Also, we formulate some open problems.
Журнал: Сибирский математический журнал
Выпуск журнала: Т. 62, № 3
Номера страниц: 619-628
ISSN журнала: 00374474
Место издания: Новосибирск
Издатель: Сибирское отделение РАН, Институт математики им. С.Л. Соболева СО РАН