Siberian Federal University

We study the satisfiability problem for a bimodal temporal logic interpreted on infinite cluster 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 clusters and represents a discrete macro-time. We prove decidability of the logic by a two-stage reduction. First, we apply local filtration with respect to the set of subformulas that do not contain global modalities; this compresses the internal structure of each cluster while preserving truth of the local fragment. Second, we establish the existence of a stability index and the correctness of a folding procedure, which replaces an infinite sequence of clusters 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 nesting depth of the global modality). As a consequence, we obtain a finite-model property with respect to the constructed class of filtered lassos and an effective satisfiability-checking procedure