M. C. Fernández-Gago, U. Hustadt, C. Dixon, M. Fisher, and B. Konev (2005): ``First-Order Temporal Verification in Practice.'' In Journal of Automated Reasoning 34:295-321.
Abstract, BibTeX, Abstract + PDF (Springer).

First-order temporal logic, the extension of first-order logic with operators dealing with time, is a powerful and expressive formalism with many potential applications. This expressive logic can be viewed as a framework in which to investigate problems specified in other logics. The monodic fragment of first-order temporal logic is a useful fragment that possesses good computational properties such as completeness and sometimes even decidability. Temporal logics of knowledge are useful for dealing with situations where the knowledge of agents in a system is involved. In this paper we present a translation from temporal logics of knowledge into the monodic fragment of first-order temporal logic. We can then use a theorem prover for monodic first-order temporal logic to prove properties of the translated formulas. This allows problems specified in temporal logics of knowledge to be verified automatically without needing a specialized theorem prover for temporal logics of knowledge. We present the translation, its correctness, and examples of its use.


Logic and Computation Group at the Department of Computer Science, University of Liverpool
Maintained by Ullrich Hustadt, U.Hustadt@csc.liv.ac.uk, last updated Friday, 16-Aug-2013 16:47:45 BST © 1998-2004 by Ullrich Hustadt.