@article {Fernandez2005, title = {First-Order Temporal Verification in Practice}, journal = {Journal of Automated Reasoning}, volume = {34}, year = {2005}, pages = {295-321}, publisher = {Springer}, abstract = {

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.

}, issn = {0168-7433}, doi = {dx.doi.org/10.1007/s10817-005-7354-1}, author = {Carmen Fernandez-Gago and Ullrich Hustadt and Clare Dixon and Michale Fisher and Boris Konev} }