    @article {Fernandez2005,
	title = {First-Order Temporal Verification in Practice},
	journal = {Journal of Automated Reasoning},
	volume = {34},
	year = {2005},
	pages = {295-321},
	publisher = {Springer},
	abstract = {<p>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.</p>
},
	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}
}
