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.

For each technical report listed here, copyright and all intellectual property rights remain with the respective authors. Copyright is effective from the year of publication in each case. By downloading a file from this page, you agree to use it only for purposes of research and scholarship. Any other use of this material or storage of it in any medium or its sale or distribution in any form is expressly forbidden without prior written permission from the authors concerned.