## Revision Note: Common Temporal Logic ConstructsA 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## PrimitivesThe following primitives are assumed: true The true operator is always true and takes one cycle.
p Boolean predicate p is true if it is satisfied by the environment.
X->Y The successor/chop operator holds if X transits to Y.
## Derived Operators
## Saftey and Liveness TheoremA 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 IdentitiesSquare and Diamond are duals of each other: []F <=> ~<>~F <>F <> ~[]~F Rules about Until <>P = true U p p U Q => <>Q ## Interval Temporal LogicInterval 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! ## Primitivesskip The skip operator always succeeds and consumes (defines) exactly one cycle.
X* The chopstar operator holds if X holds in all parts of an interval.
X;Y The chop operator holds if an ITL interval can be split such that X holds in all
of the first part and Y holds in all of the second part.
## 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 labelp 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
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 where X.SF means that SF will be true in all of the immediately succeeding states
F.SF means that SF will be eventually encountered along all subsequent paths
G.SF means that SF will be true in all states of all subsequent paths
U is the Until path diadic operator,
W is the Weak Until path operator.
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 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 OperatorsPath 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 QuantifiersCTL is a subset of CTL*. Only the following six path logic quantifier combinations can occur in CTL:
For example, 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 logicPath 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 ... ## ReferencesS. 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. |