next up previous
Next: Defeasible logic Up: System Specification Previous: Propositional modal logic

Temporal logic

A straightforward extension of tex2html_wrap_inline773 tex2html_wrap_inline947 leads to what Thayse 1989 calls linear-time temporal logic, which is not only useful in AI for modeling domains that include phenomena that vary with time (and what robust domain fails to include such phenomena?) but is also a tool for verifying the behavior of computer programs that have nothing to do with AI. The extension comes via two new operators, tex2html_wrap_inline1169 and tex2html_wrap_inline1171 ; this yields a total of four operators now, which are read as follows:

A semantical account starts with a temporal frame tex2html_wrap_inline967 = (S, R), where S is an at-most-countable, non-empty set of states, and R is a binary relation on S satisfying a condition that makes it a functional relation, viz.,

displaymath1191

(The quantifier tex2html_wrap_inline1193 essentially says `there is exactly one x such that'.) Now, using P again as the set of all atomic wffs from the propositional calculus, define a function I analogously to V from above; specifically, let I be a mapping from tex2html_wrap_inline1205 to the truth-values `true' and `false', {T, F}. (I tells us whether or not a given atomic formula p is true at a given state s.) A temporal interpretation tex2html_wrap_inline809 is then a pair tex2html_wrap_inline1215 I) that can give precise ``meaning'' to expressions in the logic, as follows. For the propositional case, a conjunction tex2html_wrap_inline1219 is true at a state s iff both p and q are true at s. This is written as tex2html_wrap_inline809 tex2html_wrap_inline1231 iff tex2html_wrap_inline809 tex2html_wrap_inline1235 and tex2html_wrap_inline809 tex2html_wrap_inline1239 . For the interesting cases, the operators, we let tex2html_wrap_inline1241 denote the (i+1)st member of the sequence

displaymath1245

Then, for example,

As Thayse 1989 shows, formulas that, intuitively, we would want to come out valid on this scheme--e.g., tex2html_wrap_inline1265 , a counterpart to axiom K in tex2html_wrap_inline773 tex2html_wrap_inline947 --do come out valid, formally speaking. Thayse 1989 and Thayse 1991 also consider, in informative detail, how to go about proving things in linear-time temporal logic (and in enhancements of it). We return to some of the metatheory for this logic below.

We should mention that temporal logic is by no means the only tool used in AI for enabling reasoning about time and change. In fact, AI has often tended to refer to the entities posited in temporal logic (e.g., events, possible worlds, or histories) directly in modifications of tex2html_wrap_inline773 tex2html_wrap_inline775 . The earliest such formalism was the situation calculus, invented by John McCarthy (1968); a good presentation of this formalism, modernized from the form it had when first presented, can be found in Genesereth & Nilsson 1987. The paper ``Nonmonotonic Reasoning in the Framework of the Situation Calculus'', by Andrew Baker, found in the Brachman et al. volume, provides a quick but serviceable introduction to the situation calculus at work. Another well-known approach in AI to reasoning about time and change comes by way of James Allen's ``interval approach'' (1984). Rina Dechter, Itay Meiri, and Judea Pearl's ``Temporal Constraint Networks'', in Brachman et al. shows another (advanced) approach to time and action, one based on networks; the authors compare their approach to Allen's.

When temporal logic is deployed to systematize reasoning about the behavior of computer programs, it is often recast as dynamic logic, wherein the operators we have identified are associated with commands in a programming language. For a short but elegant description of dynamic logic as reinterpretation of temporal logic, see Thayse 1989 itself.


next up previous
Next: Defeasible logic Up: System Specification Previous: Propositional modal logic

Selmer Bringsjord
Mon Nov 17 14:57:06 EST 1997