Bisimulation, unravellings and covers

Bisimulation equivalences and associated model construction techniques - in particular the so-called "unravellings" - play a crucial role in the model theory of modal and guarded logics. 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 of corresponding new results 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.