Notes on Modal and Temporal Logics

By Micah Lewis, Rahul Kumar, and Kevin Simonson

Background

Modal logic was originally developed to investigate logic under the modes of necessary and possible truth.  The words "necessary" and "possible" are called modal connectives, or modalities.  A modality is a word that when applied to a statement indicates when, where, how, or under what circumstances the statement may be true.  In terms of notation, it is common to use a box [] for the modality "necessary" and a diamond <> for the modality "possible".  Applying the negation connective we can express the relation between the two modalities as follows:  <> = ¬[]¬ and similarly [] = ¬<>¬.

Modal languages have been found to be very useful in reasoning about relational structures that are frequently used in mathematics and computer science as well as other areas.  A relational structure is a structure defined by a set and a collection of relations.  An example of a relational structure is (N , <), the set of natural numbers ordered by the less-than-or-equal-to relation.  One of the most common relational structures used in computer science is the labeled transition system (LTS).  A labeled transition system is composed of a set of nodes, labels, and a corresponding relation for each label that relates pairs of nodes.

The Basic Modal Language
The grammar for the basic modal language is given below:
ø ::= p | F  |  ¬ø  |  ß or ø  |  <>ø  
The letter p is an element of the set of proposition letters and F represents the constant false value.  According to the grammar, modal formulas allow negation, disjunction and a formula prefixed by the modality diamond.  More complex modal languages extend the basic modal language with operators and other symbols -- such as temporal languages used in model checking.

Frames and Models
The notion of a frame is used in modal languages to reason about valid formulas.  Frames are just relational structures composed of a non-empty set W which represents the domain or universe of the relational structure and a binary relation R on W.  A frame F is therefore the pair (W, R).

Models are the structure used to discuss satisfiability.  A model for the basic modal language is defined as a frame F and a valuation function V that given a proposition letter p returns a subset of W.  Intuitively, V(p) returns the set of states in W where p is true.  It should be clear that the relationship between models and frames is that for a given frame F, there may exist many models M which are based on F.  For a given M, however, there exists only one frame F.  

Satisfiability
Blackburn et al. give an inductive definition of satisfiability which we present here.
Definition: Suppose w is a state in a model M = (W, R, V).  Then we inductively define the notion of a formula ø being satisfied (or true) in M at state w as follows:
M,w ||- p iff w is an element of V(p), where p is a propositional letter,
M,w ||- F never,
M,w ||- ¬ø iff not M,w ||- ø,
M,w ||-  ø  or ß iff M,w ||-  ø   or   M,w  ||- ß,
M,w ||-  <> ø iff for some v in W with Rwv we have M,v  ||-   ø.

The notation ||- is supposed to be the turn-style symbol which can be read as "satisfies".

It should be noted that evaluating a formula begins at some state w and proceeds to its successors.  For this reason, satisfaction is considered to be local and internal to the model.  If a formula is true starting from every state in a model, then it is universally true.  For a formula to be considered satisfiable, there must exist at least one state in the model at which the formula is true.

Validity
Validity in modal languages is defined at the level of frames.  A formula is valid in a frame F if it is universally true in every model based on F.  We can also say that a formula is valid in a state w if it is true in every state w of every model based on F.  

"Validity" is a different concept than that of "truth". If we know that p \/ q is true, then by definition either p is true or q is true. On the other hand, if we know that p \/ q is valid on frame F, that does not mean that either p or q is valid on frame F. To say that either p or q is valid on frame F would mean that either p or q is true in every model (F, V) based on F, and in reality there might be some models where p is true and some where q is true; in that case it would be an error to say that either p or q is valid on F; in reality neither is valid on F.

Modal Satisfaction in Models
Three different structures that can be created from models are a disjoint union, bounded morphism, and a generated submodel (refer to Glossary ).   All three of them preserve the modal properties of the structures from which they were constructed.  

Disjoint Union
Assume the existence of directed graphs A and B.  A disjoint union is nothing more than combining A and B into a structure C with things relabeled as necessary to prevent A and B from conflicting.  The structure C would contain two mutually exclusive structures.  It is obvious that any property satisfiable in either A or B will also be satisfiable in C.

Generated Submodel
A generated submodel, on the other hand, is the result of removing parts of a model to get a reduced model that retains all the necessary properties of its predecessor.  Given two models A and B, we would say that B is a generated submodel of A if for every state w in A, if w is in B and w is related to v in A by the relation Rwv, then v is also in B.  Generated submodels are useful to reduce a rather large model to something more manageable while still preserving interesting properties.

Morphisms
Morphisms generally refer to functions that map between two structures and in some manner preserve structure.  There are different kinds of morphisms, the most simple being a homomorphism.  A homomorphism is a mapping function f: M -> M' in which relations in the source model, M, are present in the target, M'.  This does not preclude the target from containing extra relations and therefore does not imply that the structure of the target is reflected in the source.  A strong homomorphism between a model M and M' is when the structure of M is preserved in M' and vice-versa.  Since morphisms refer to mapping, with the domain as the set of models M and the range as the set of models M' , when the morphism is a bijective (surjective and injective) strong homomorphism we call it an isomorphism.  In mathematics, an isomorphism means "mathematically identical".

A bounded morphism is a mapping f : M = (W, R, V) -> M' = (W', R', V') that satisfies the following conditions:
  1. w and f(w) satisfy the same proposition letters.
  2. For all modal operators i in the modal language, Riwv1 ... vn implies Ri' f(w)f(v1) ... f(vn).
  3. If Ri' f(w)v'1 ... v'n then there exist v1 ... vn such that Riwv1 ... vn and f(vi) = v'i (for 1 < i < n).
The second condition of the definition is called the homorphic condition and preserves relations from the source to the target while the third condition is the back condition and guarantees that some structure of the target is reflected in the source.  If a bounded morphism from M to M' is surjective, it is called a bounded morphic image [Blackburn].

Bisimulations

A bisimulation is a relation between two transition systems such that one simulates the behavior of the other and vice-versa.  Stated another way, a bisimulation between models is when related states have identical atomic information and matching transition possibilities [Blackburn].  Bisimulation between models / transition systems indicates that they are computationally equivalent.  This means that given a modal formula and two bisimilar models, evaluating the formula in either model will provide the same result.  This concept is useful in areas of computer science such as Model Checking where abstraction techniques are applied to a model of a computer program or electrical circuit in order to produce a reduced model.  When the reduced model is bisimilar to the original, all the properties of the original are guaranteed to be present.  In other words, modal formulas are invariant under bisimulations.  

The same is not true of first-order logic formulas.  They are not guaranteed to be invariant under bisimulation.  As is often the case, mathematicians are interested in knowing the relation between first-order logic and modal logic.  Although not explained here, the van Benthem Characterization Theorem provides the result that modal logic is the bisimulation invariant fragment of first-order logic [Blackburn].  This means that given the set of all models and all bisimulations between every model, the set of first-order formulas that are invariant under every bisimulation is modal logic.

Hennesy-Milner Theorem
Let T be a modal similarity type, and let M and M' be two image-finite T models. Then for every w that belongs to W and w' that belongs to W', w is bisimilar to w' iff w is modally equivalent to w'. The proof can be looked at in detail in  Modal Logic by Blackburn.

Propositional Temporal Logic

Propositional Temporal Logic redefines []A to mean "A holds at all time points after the reference point," and <>A to mean "There is a time point after the reference point at which A holds." In addition it adds a circle operator; oA means "A holds at the time point immediately after the reference point." And it adds an atnext operator; A atnext B means "A will hold at the next time point that B holds."

Interestingly, each of o, [], and <> can be defined using the basic logical connectives and atnext. oA is simply A atnext true; []A is simply A /\ false atnext ¬A; and of course <>A is just ¬[]¬A.

Logic Semantics

The precise semantics of Propositional Temporal Logic involve a temporal structure (also called Kripke structure) that I'll call K. K is made up of a series of functions Ki, with i any natural number. Ki is a mapping from all possible temporal formulas to the set {f, t}. Each structure Ki assigns a true value to different atomic variables, and similarly false values, but once those values are defined for the atomic variables the rest of Ki is defined by:

Ki(¬A) = t iff Ki(A) = f
Ki(A -> B) = t iff Ki(A) = f or Ki(B) = t
Ki(oA) = t iff Ki+1(A) = t
Ki([]A) = t iff Kj(A) = t for every j >i
Ki(A atnext B) = t iff Kj(B) = f for every j > i, or Kk(A) = t for the smallest k > i with Kk(B) = t.

Axiomatization

The following are five axioms which, combined with the tautologies of ordinary logic, can be used to prove all theorems of temporal logic.

¬oA <-> o¬A
o(A -> B) -> (oA -> oB)
[]A -> A /\ o[]A
o[]¬B -> A atnext B
A atnext B <-> o(B -> A) /\ o(¬B -> A atnext B)

The rules used to generate theorems from prior axioms or theorems are:

A, A -> B |- B
A |- oA
A -> B, A -> oA |- A -> []B

For the record I don't understand why the second rule works. It seems to say that if a formula is true at time t then it also must be true at time t+1. That doesn't make sense at all.

Temporal Semantics of Programs

Properties we would like to verify with programs can be roughly divided into two categories, safety properties and liveness properties. Informally, safety properties are guarantees that nothing bad will happen, whereas liveness properties are guarantees that something good will happen eventually. Understandably, then, safety properties are all of the form A -> []B, and liveness properties are all of the form A -> <>B. Interestingly, partial correctness is listed as a safety property, while total correctness is listed as a liveness property. This actually makes sense since partial correctness simply asserts that if a program terminates it's guaranteed to terminate with some property holding, while total correctness asserts that at some future point the program will terminate with that property holding.

Provability as a Modality
Glossary of terms
Reading List