First-Order Temporal Verification in Practice. Fernández-Gago, M. C., Hustadt, U., Dixon, C., Fisher, M., & Konev, B. Journal of Automated Reasoning, 34(3):295-321, April, 2005.
Paper abstract bibtex 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.
@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.}
}