Paper  abstract   bibtex   

@ARTICLE{Fernandez-Gago+Hustadt+Dixon+Fisher+Konev@JAR2005,
 AUTHOR        = {M. C. Fern{\'a}ndez-Gago and U. Hustadt and C. Dixon 
 and M. Fisher and B. Konev},
 TITLE         = {First-Order Temporal Verification in Practice},
 JOURNAL       = {Journal of Automated Reasoning},
 YEAR          = {2005},
 VOLUME        = {34},
 NUMBER        = {3},
 PAGES         = {295-321},
 MONTH         = apr,
 URL           = {http://dx.doi.org/10.1007/s10817-005-7354-1},
 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.}
}