Tech Reports

ULCS-09-009

Characterising Finite Domains in Monodic First-Order Temporal Logic

Boris Konev, Anatoli Degtiarev, Michael Fisher and Alexei Lisitsa


Abstract

In this paper we introduce a syntactic characterisation of finite domains in first-order temporal logics. In addition to showing that this characterisation is complete with respect to finite domains, we show that the formulae are still within a decidable fragment of first-order temporal logic. This allows us to automatically verify certain finite properties of temporal specifications simply by adding the characteristic formula to the specification and carrying out verification as usual.

[Full Paper]