Temporal Logic has achieved a significant role in Computer Science, in particular, within the formal specification and verification of concurrent and distributed systems [19, 18, 14]. While First-Order Temporal Logic (FOTL) is a very powerful and expressive formalism in which the specification of many algorithms, protocols and computational systems can be given at the natural level of abstraction, most of the temporal logics used remain essentially propositional. The reason for this is that it is easy to show that FOTL is, in general, incomplete (that is, not recursively-enumerable [21]). In fact, until recently, it has been difficult to find any non-trivial fragment of FOTL that has reasonable properties. A breakthrough by Hodkinson et. al.[13] showed that monodic fragments of FOTL could be complete, even decidable. Over a number of years we have been developing software tools [15, 16] for automated reasoning in this logic and working on the deductive approach to verification using the monodic fragment. Our applications are in areas as diverse as agent-based systems, distributed architectures, and security. Based on our earlier work on propositional logic [9], we extended our proof techniques to cover first-order aspects [2] and, hence, the possibility of verifying, deductively, parametrised and infinite state problems. In [10], we suggested a theoretical basis for translating a general protocol model for infinite number of processes into the monodic fragment. However, while being shown to be possible, no full proof was carried out. The main contribution of this paper is to present our first attempts to apply previously developed methods and existing software tools to realistic infinite-state verification problems. Since we encountered difficulties, in particular, concerning the use of equality, we also tackle these technical problems in the paper.

We begin by describing the particular form of first-order temporal logic (FOTL) that we use. Following this, we describe a general model of infinite state protocols and show how both the protocol, and appropriate correctness conditions, can be translated into FOTL. Next, we describe how problems with equality can sometimes be avoided in practical temporal reasoning, and consider a simple infinite state protocol based on the finite state machine model of cache coherence protocols presented in [4]. Finally, we provide concluding remarks and outline future work.