@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.}
}

{"_id":"7hqtEanCBvqwKkLvH","bibbaseid":"fernndezgago-hustadt-dixon-fisher-konev-firstordertemporalverificationinpractice-2005","author_short":["Fernández-Gago, M. C.","Hustadt, U.","Dixon, C.","Fisher, M.","Konev, B."],"bibdata":{"bibtype":"article","type":"article","author":[{"firstnames":["M.","C."],"propositions":[],"lastnames":["Fernández-Gago"],"suffixes":[]},{"firstnames":["U."],"propositions":[],"lastnames":["Hustadt"],"suffixes":[]},{"firstnames":["C."],"propositions":[],"lastnames":["Dixon"],"suffixes":[]},{"firstnames":["M."],"propositions":[],"lastnames":["Fisher"],"suffixes":[]},{"firstnames":["B."],"propositions":[],"lastnames":["Konev"],"suffixes":[]}],"title":"First-Order Temporal Verification in Practice","journal":"Journal of Automated Reasoning","year":"2005","volume":"34","number":"3","pages":"295-321","month":"April","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.","bibtex":"@ARTICLE{Fernandez-Gago+Hustadt+Dixon+Fisher+Konev@JAR2005,\n AUTHOR = {M. C. Fern{\\'a}ndez-Gago and U. Hustadt and C. Dixon \n and M. Fisher and B. Konev},\n TITLE = {First-Order Temporal Verification in Practice},\n JOURNAL = {Journal of Automated Reasoning},\n YEAR = {2005},\n VOLUME = {34},\n NUMBER = {3},\n PAGES = {295-321},\n MONTH = apr,\n URL = {http://dx.doi.org/10.1007/s10817-005-7354-1},\n ABSTRACT = {First-order temporal logic, the extension \n of first-order logic with operators dealing with time, is a \n powerful and expressive formalism with many potential \n applications. This expressive logic can be viewed as a \n framework in which to investigate problems specified in \n other logics. The monodic fragment of first-order temporal \n logic is a useful fragment that possesses good computational \n properties such as completeness and sometimes even decidability. \n Temporal logics of knowledge are useful for dealing with situations \n where the knowledge of agents in a system is involved. In this \n paper we present a translation from temporal logics of knowledge \n into the monodic fragment of first-order temporal logic. We can \n then use a theorem prover for monodic first-order temporal logic \n to prove properties of the translated formulas. This allows problems \n specified in temporal logics of knowledge to be verified automatically \n without needing a specialized theorem prover for temporal logics of \n knowledge. We present the translation, its correctness, and examples \n of its use.}\n}\n","author_short":["Fernández-Gago, M. C.","Hustadt, U.","Dixon, C.","Fisher, M.","Konev, B."],"key":"Fernandez-Gago+Hustadt+Dixon+Fisher+Konev@JAR2005","id":"Fernandez-Gago+Hustadt+Dixon+Fisher+Konev@JAR2005","bibbaseid":"fernndezgago-hustadt-dixon-fisher-konev-firstordertemporalverificationinpractice-2005","role":"author","urls":{"Paper":"http://dx.doi.org/10.1007/s10817-005-7354-1"},"metadata":{"authorlinks":{}}},"bibtype":"article","biburl":"http://cgi.csc.liv.ac.uk/~ullrich/publications/all.bib?authorFirst=1","dataSources":["WhiGijHmCtTSdLaAj"],"keywords":[],"search_terms":["first","order","temporal","verification","practice","fernández-gago","hustadt","dixon","fisher","konev"],"title":"First-Order Temporal Verification in Practice","year":2005}