Тип публикации: статья из журнала
Год издания: 2026
Ключевые слова: Bimodal logic, local filtration, stability index, temporal degree, model folding, decidability, бимодальная логика, локальная фильтрация, индекс стабильности, темпоральная степень, свёртка модели, разрешимость
Аннотация: We study the satisfiability problem for a bimodal temporal logic interpreted on infinitecluster frames of the form W = ⊔ i∈ N C ( i ). Each cluster C ( i ) is an arbitrary (possibly infinite) Kripke frame with a reflexive and transitive local relation, while the global relation linearly orders the clustersand represents a discrete Показать полностьюmacro-time. We prove decidability of the logic by a two-stage reduction. First, we apply local filtration withrespect to the set of subformulas that do not contain global modalities; this compresses the internalstructure of each cluster while preserving truth of the local fragment. Second, we establish the existenceof a stability index and the correctness of a folding procedure, which replaces an infinite sequence ofclusters by a finite lasso-shaped structure without loss of truth for the input formula. Correctness of folding is proved by induction on the temporal degree of a formula (the nestingdepth of the global modality). As a consequence, we obtain a finite-model property with respect to theconstructed class of filtered lassos and an effective satisfiability-checking procedure В работе исследуется задача выполнимости для бимодальной темпоральной логикина бесконечных кластерных шкалах, где глобальное отношение упорядочивает кластеры, а локальное отношение внутри каждого кластера является рефлексивным и транзитивным. Доказывается разрешимость с помощью двухэтапного сведения: локальной фильтрации по подформуламбез глобальных модальностей и последующей стабилизации типов кластеров с построением конечной «лассо»-модели. Корректность свёртки доказывается индукцией по темпоральной степениформулы (глубине вложенности глобальной модальности), что даёт конечномодельное свойство иэффективную процедуру проверки выполнимости
Журнал: Журнал Сибирского федерального университета. Серия: Математика и физика
Выпуск журнала: Т.19, №3
Номера страниц: 417-422
ISSN журнала: 19971397
Место издания: Красноярск
Издатель: Сибирский федеральный университет