Сибирский федеральный университет

В работе исследуется задача выполнимости для бимодальной темпоральной логики на бесконечных кластерных шкалах, где глобальное отношение упорядочивает кластеры, а локальное отношение внутри каждого кластера является рефлексивным и транзитивным. Доказывается разрешимость с помощью двухэтапного сведения: локальной фильтрации по подформулам без глобальных модальностей и последующей стабилизации типов кластеров с построением конечной «лассо»-модели. Корректность свёртки доказывается индукцией по темпоральной степени формулы (глубине вложенности глобальной модальности), что даёт конечномодельное свойство и эффективную процедуру проверки выполнимости