Department of Computer Science
University of Wales
4pm Tuesday 28th May 2002
Room 2511, JCMB, King's Buildings
Many model theoretic arguments for modal logics rely on bisimulation invariance which can be used to prepare nice tree-like models. Much of the usefulness of modal logics and their good algorithmic behaviour may directly be attributed to this fact (tree model property). And indeed, tree models can be obtained as bisimilar unravellings of any given model. Similar techniques apply to guarded logics, which are more expressive relatives of modal logics, with their corresponding notion of bisimulation. As tree-like unravellings are typically infinite, however, they are not so useful in 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) with some applications to semantic characterisation theorems, to the finite model property of guarded logics, and links with extension properties for partial isomorphisms.