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.
