The Freedoms of (Guarded) Bisimulation

Abstract

We survey different notions of bisimulation equivalence that provide flexible and powerful concepts for understanding the expressive power as well as the model-theoretic and algorithmic properties of modal logics and of more and more powerful variants of guarded logics. An appropriate notion of bisimulation for a logic allows us to study the expressive power of that logic in terms of semantic invariance and logical indistinguishability. As bisimilar nodes or tuples in two structures cannot be distinguished by formulae of the logic, bisimulations may be used to control the complexity of the models under consideration. In this manner, bisimulation-respecting model constructions and transformations lead to results about model-theoretic properties of modal and guarded logics, such as the tree model property of modal logics and the fact that satisfiable guarded formulae have models of bounded tree width. A highlight of the bisimulation-based analysis are the characterisation theorems: inside a classical level of logical expressiveness such as first-order or monadic second-order definability, these provide a tight match between bisimulation invariance and logical definability. Typically such characterisation theorems state that a modal or guarded logic is not only invariant under bisimulation but, conversely, also expressively complete for the class of all bisimulation invariant properties at that level. Finally, the bisimulation-based analysis of modal and guarded logics also leads to important insights concerning their algorithmic properties. Since satisfiable formulae always admit simple models, for instance tree-like ones, and since modal and guarded logics can be embedded or interpreted in monadic second-order logic on trees, powerful automata theoretic methods become available for checking satisfiability and for evaluating formulae.