Tim French

Bisimulation quantifiers for modal logics

Bisimulation quantifiers in modal logics allow us to quantify over the interpretation of an atom in all bisimilar models belonging to the logic. Consequently they are generally weaker than normal propositional quantification, and more likely to produce decidable logics. We first present some negative results, giving cases where bisimulation quantified modal logics are not bisimulation invariant, and cases where bisimulation quantifiers do not preserve decidability. We then focus on some positive results, giving a sufficient condition for bisimulation quantified modal logics to be bisimulation invariant, and discussing methods for defining new decidable bisimulation quantified modal logics using methods from monadic second-order logics.