Modal and guarded characterisation theorems over finite transition systems

Martin Otto

To appear at Symposium on Logic in Computer Science (LICS'2002), Copenhagen, Denmark, July 22nd - 25th, 2002


Characterisation theorems for modal and guarded fragments of first-order logic are explored over finite transition systems. We show that the classical characterisations in terms of semantic invariance under the appropriate forms of bisimulation equivalence can be recovered at the level of finite model theory. The new, more constructive proofs naturally extend to alternative proofs of the classical variants. A finite model theory version of van Benthem's characterisation theorem for basic modal logic, which similarly sheds new light on the classical version, is due to E.Rosen. That proof is simplified and the result slightly strengthened in terms of quantitative bounds with the new approach presented here. The main thrust of the present paper, however, lies in a uniform treatment that extends to incorporate universal and inverse modalities and guarded quantification over transition systems (width two relational structures). Apart from first-order locality (specific ramifications of Gaifman's theorem for bisimulation invariant formulae) our treatment rests on a natural construction of finite, locally acyclic covers for finite transition systems. These covers can serve as finite analogues of tree unravellings in providing local control over first-order logic in finite bisimilar companion structures.

Server START Conference Manager
Update Time 15 Mar 2002 at 15:30:29
Start Conference Manager
Conference Systems