Bisimulation, Unravellings, Covers

Martin Otto

Notions of bisimulation equivalence play a crucial role in any account of the good behaviour of modal and guarded logics, and explain much of their manifold applicability, ranging from verification to knowledge respresentation. Associated model construction techniques that preserve the bisimulation type while otherwise simplifying structure allow us pass to "nice" models behind the logics' back. This is particularly evident in so-called "unravellings" that lead to very tractable, albeit infinite, tree-like models.

A number of related issues in the finite model theory of these logics raise the question to which extent similar methods can be employed even when we do not admit infinite models. With this talk I take a look at some of the combinatorial issues involved, and at some applications to questions ranging from the semantic characterisation of modal and guarded logics over finite transition systems to extension theorems for local isomorphisms, and to the finite model property of guarded logics.