Intransitive temporal multi-agent logic with agents' multi-valuations. Decidability

Изучается нетранзитивная временная мультиагентная логика с мультиозначиваниями агентов для переменных и формул. Ранее время и знания моделировались с помощью моделей Крипке, структура которых выглядела как простой единый временной кластер с множеством отношений достижимости для агентов. Здесь мы развиваем этот подход и используем модели Крипке, которые представляют собой линейное нетранзитивное время и состояния, представленные произвольными временными кластерами для мультиотношений достижимости агентов. Эта логика определяется семантически как множество формул, истинных на линейных моделях с мультиозначиваниями переменными и кластерами состояний. Мы предлагаем обоснование такого подхода и методику вычисления истинностных значений формул. Основные результаты касаются проблемы разрешимости. Мы доказываем, что полученная логика разрешима и финитно аппроксимируема.