Next: Defeasible logic Up: System Specification Previous: Propositional modal logic

## Temporal logic

A straightforward extension of 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, and ; this yields a total of four operators now, which are read as follows:

• - at the next time
• - always
• - eventually
• - until
A semantical account starts with a temporal frame = (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.,

(The quantifier 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 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 is then a pair I) that can give precise ``meaning'' to expressions in the logic, as follows. For the propositional case, a conjunction is true at a state s iff both p and q are true at s. This is written as iff and . For the interesting cases, the operators, we let denote the (i+1)st member of the sequence

Then, for example,

• = T iff = T, and
• = T iff = T,
As Thayse 1989 shows, formulas that, intuitively, we would want to come out valid on this scheme--e.g., , a counterpart to axiom K in --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 . 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: Defeasible logic Up: System Specification Previous: Propositional modal logic

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