Equivalence Criteria for Compositional IF Modal Logics
Tero Tulenheimo, Manuel Rebuschi · Electronic Notes in Theoretical Computer Science · 2009
An IF modal logic L with a compositional semantics is formulated, generalizing the logic LSD introduced in [T. Tulenheimo, and M. Sevenster, On modal logic, IF logic and IF modal logic, in G. Governatori et al. (eds.): “Advances in Modal Logic” 6, 481–501, College Publications, 2006]. Syntactic fragments L1, L2, L3, L4 are discerned. For each fragment, we study the relation of Li-equivalence: an equivalence relation between pointed models holding if and only if they satisfy precisely the same formulas of Li. A criterion for Li-equivalence is formulated in terms of model-comparison games, by imposing further conditions in addition to bisimilarity. Using the resulting methods for establishing indistinguishability w.r.t. Li, the relative expressive powers of the four fragments are determined.