Revision Note: Common Temporal Logic Constructs
A number of different basis sets for temporal logic are possible and a number of restrictions on the allowable uses of negation and quantification lead to various classes of temporal logic. Here are some notes I blogged.
A Linear Temporal Logic formula describes a pattern for a sequence of events. Any actual sequence of events may match or not match that pattern. A Branching Temporal Logic formula is more expressive, since it may contain quantifiers that range over a number of possible sequences.
Common Linear Temporal Logic (LTL) Operators
The following primitives are assumed:
Saftey and Liveness Theorem
A safety property is an assertion that a particular state will not be reached.
A liveness property is that a particular state will always be reachable regardless of the current state.
The SL theorem is that any LTL formula can be expressed as a conjunction of a safety and a liveness property.
Important LTL Identities
Square and Diamond are duals of each other:
F <=> ~<>~F <>F <> ~~F
Rules about Until
<>P = true U p p U Q => <>Q
Interval Temporal Logic
Interval Temporal Logic is a variation on LTL temporal logic where formulae apply to closed intervals rather than infinite futures. However, the presence of the star operator allows the intervals to be infinitely long!
Derived ITL operator table:
Branching Time Path Logics (CTL and CTL*)
A path is a sequence of states. At each state a state formula can be evaluated. A branching time path formula ranges over possible sequences of successive states.
CTL* State and Path FormulaeStates have labels. If the current state has a label p then atomic state formula p is true at that state. State formulae are built up from these atomic formualae using the Boolean connectives and the path logic quantifiers with the restriction that we cannot negate a path logic quantifier in a state formula. (Negation can effectively be applied to conjunctions and disjunctions by using negative-normal form).
SF ::= p | ~p | true | false | SF \/ SF | SF /\ SF | A.PF | E.PF
A.PF means for all paths leading from the current state, the path formula PF holds.
E.PF means for some of the paths leading from the current state, the path formula PF holds.
The path formulae have the following forms
PF ::= SF | PF /\ PF | PF \/ PF | PF U PF | PF W PF | X.SF | F.SF | G.SF
Note that it is impossible to construct an expression that negates a quantifier using the above syntax, but negations can be introduced by substituting from identities given below. Negations can (mostly/completely?) be avoided by using the W (weak until) operator instead.
Of the five specialist operators, three may be created from the X and U operators using identities and so do not need to be primitive. The identities are:
F.SF = true U SF (eventually) G.SF = false W SF (always) a W b = ~a U ~b (weak until)
Path Until Operators
Path formula use two forms of the Until operator.
The Until operator can be read as follows:
a U b = a is true in all states up until ...
The Weak Until operator can be read as follows:
a W b = as long as a is false, b must be true.
CTL: Restricted Path Logic Quantifiers
CTL is a subset of CTL*. Only the following six path logic quantifier combinations can occur in CTL:
For example, AX.g means that state formula g is true in the next state of all paths leading from the current state.
CTL is restrictive in that these letters must appear strictly as digraphs, the first always being A or E and the second always being one of the other three, making a total of six combinations.
Owing to this restriction, symbolic model checking of CTL formulae is straightforward.
Each of the quantifiers is a dual of another one, via double negation:
The F and G quantifiers are trivial forms of the until operator (McMillan thesis page 29)
Relating path logic to temporal logic
Path logics are closely related to temporal logic ...
Safety Automata (Merz)
By restricting the use of disjunction, Merz has produced results regarding 'deterministic safety automata'. He argues that temporal logic formulae can always be expressed as a conjunction of a safety and a liveness formula and that, normally, all useful properties can be expressed using only the safety half. His logic consists of the following constructs, that contain the deliberate omission of the disjunction operator between SF:
AF ::= p | ~p | true | false | AF \/ AF | AF /\ AF SF ::= AF | AF -> SF | vX.SF | o SF | SF /\ SF
Merz is able to represent the following operators and convert them into finite state automata, as shown in this table:
The `eventually' operator cannot be represented in his subset (this is readily seen by attempting to fold in the negations from the duality identity with always `<>F = ~~F'), but instead it is possible to synthesise automata ...
S. Merz. Efficiently Executable Temporal Logic Programs. (In this volume.)55. S. Merz. Decidability and Incompleteness Results for First-Order Temporal Logics of Linear Time. In Journal of Applied Non-Classical Logics, 2(2), 1992. 56. B. Moszkowski. Reasoning about digital circuits. PhD Thesis, Stanford University, July1983.