(Last modified Thu Jun 05 23:50 2008)

First-order logic is primarily concerned with truth and its negation.  Modal logic additionally considers the concepts of possibility and necessity.  If α is a FOL formula, then α is a modal logic formula that asserts that α is possibly true, and α is a modal logic formula that asserts that α is necessarily true. 

The meaning of modal logic formulae is expressed more formally in terms of "possible worlds"; α asserts that α is true in some possible world reachable from this one, while α asserts that α is true in all possible worlds reachable from this one.  is analogous to ∃, and is analogous to ∀, but that the modal logic operators quantify over possible worlds rather than over domain objects.  In addition, modal quantification is not over all possible worlds, but only over worlds reachable from the initial world; "reachable" may be interpreted in a variety of different ways, depending on the type of modal logic under consideration.  Finally, and are related by

α = ¬¬α
α = ¬¬α

Temporal logic

In computer science, modal logic is most often encountered in the form of temporal logic (TL), a modal logic in which α asserts that α is eventually true in the future, and α asserts that α is always true in the future.  Other operators may be present as well. 

There are a number of TLs, which differ to a certain extent in the temporal operators they support but more fundamentally in the model of time they assume. 

Operators

Temporal logics introduce operators typically drawn from the ones described below. 

Some common temporal logic operators

Future		Past
operator	informally	operator	informally
φ Fφ	φ will be true at some time in the future	φ Pφ	φ was true at some time in the past
φ Gφ	φ will always be true in the future	φ Hφ	φ was always true in the past
If < on time is transitive and nonreflexive:
φUχ φ until χ	φ will always be true until χ becomes true	φSχ φ since χ	χ was always true until φ became true
φ	φ will be true "next"	φ	φ was true "previously"

Examples of , ,

Time	α	α	β	β	γ	γ
0	tt	tt	ff	tt	tt	tt
1	tt	tt	ff	tt	tt	tt
2	tt	tt	ff	tt	tt	tt
3	tt	tt	ff	tt	tt	ff
4	tt	tt	tt	tt	ff	ff
...	tt	tt	tt	tt	ff	ff

Structure of time

Unlike FOL, whose models have a single well-defined structure, there are a number of model structures for TL, varying in how they represent the possibilities of time.  The possibilities are:

1. Does time follow a linear course, or can it branch in either the future direction or the past?
2. Is time dense or discrete?  Time is dense if between any two instants there is always a third instant. 
3. Does time extend without limit in either or both directions?

Formally expressing the structure of time

Some time structures

Let r, s, t, and u be instants in time.  The structure of time can be described by the following properties. 

begin

This property is true if time has a first instant. 

∃t [ ¬∃s(s<t) ]

end

This property is true if time has a last instant. 

∃s [ ¬∃t(s<t) ]

dense

This property is true with respect to < if any two instants always have another instant between them. 

∀s u [ ¬(s<u) ∨ ∃t (s<t ∧ t<v) ]

linear

This property is true if time is linear, and thus totally ordered. 

∀s t [ (s < t) ∨ (s = t) ∨ (s > t) ]

left linear

This property is true if time can branch to the right, and is thus partially ordered. 

∀s t u ( ¬ [ (s < u) ∧ (t < u) ] ∨ (s < t) ∨ (s = t) ∨ (s > t) )

right linear

This property is true if time can branch to the left, and is thus partially ordered. 

∀r s t ( ¬ [ (r < s) ∧ (r < t) ] ∨ (s < t) ∨ (s = t) ∨ (s > t) )

¬"I have pressed a call button"∨"The elevator opens its doors at my floor". 

Thomas A. Alspaugh
Assistant Professor, Informatics Dept.
School of Information and Computer Sciences