28 June 2002, ILLC talks, Martin Otto

Abstract:

Many model theoretic arguments for modal logics rely on bisimulation invariance which can be used to prepare nice tree-like models. The resulting tree model property of modal logics plays a major part in the usefulness and good algorithmic behaviour of modal logics. Tree models are in fact quite simply obtained as bisimilar unravellings of any given models. As bisimilar unravellings are typically infinite, however, they are not suited to the context of finite model theory. Instead, one needs other nice and manageable bisimilar companion structures that can be kept finite.

In this talk I shall discuss such constructions (and related open problems) primarily with applications to semantic characterisation theorems. Other applications, in particular also related to guarded logics, provide links with extension properties for partial isomorphisms and the finite model property of guarded logics. At the methodological level, these issues serve to illustrate the power of logic games in the model theoretic study of semantic invariances that go hand in hand with corresponding model constructions and model transformations.