Logic in Computer Science (LICS 2002)

Paper: Modal and guarded characterisation theorems over finite transition systems (at LICS 2002)

Authors: Martin Otto

Abstract

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.

BibTeX

  @InProceedings{Otto-Modalandguardedchar,
    author = 	 {Martin Otto},
    title = 	 {Modal and guarded characterisation theorems over finite
    transition systems},
    booktitle =  {Proceedings of the Seventeenth Annual IEEE Symp. on Logic in Computer Science, {LICS} 2002},
    year =	 2002,
    editor =	 {Gordon Plotkin},
    month =	 {July}, 
    location =   {Copenhagen, Denmark}, 
    publisher =	 {IEEE Computer Society Press}
  }