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

Primitives

The 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

        o     circle / next state     oF = skip;F
        <>F     diamond / eventually     <>F = true*;F
        <w>F     weak next     <w>F = ~(o(~F))
        []F     square / always     []F
        upto     upto     F upto G
        F U G     until     F U G =
        F W G     unless / weak until     F W G
        atnext     atnext     F atnext G
        leadsto     leadsto     F leadsto G = [](F -> <>G)

    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!

    Primitives

  • skip 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:

    Operator Symbol Name Use Expands To
        o     circle / next state     oF skip;F
        <>F     diamond / eventually     <>F true*;F
        <w>F     weak next     <w>F ~(o(~F))
        []F     square / always     []F ~(<>(~F))
        upto     upto     F upto G
        F U G     until     F U G
        F W G     unless / weak until     F W G
        atnext     atnext     F atnext G
        leadsto     leadsto     F leadsto G [](F -> <>G)

    ITL Homepage


    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 Formulae

    States 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   
    

    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 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:

    A for all
    E for some
    followed by one of
    X next
    F eventually
    G always

    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:

    AF.g     ~EG.~g
    AG.g     ~EF.~g
    AX.g     ~EX.~g

    The F and G quantifiers are trivial forms of the until operator (McMillan thesis page 29)

    AF.g     A(true U g)
    EF.g     E(true U g)
    AG.g     ~E(true U ~g)
    EG.g     ~A(true U ~g)

    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:

    Operator Symbol Name Use Automata Construction
        o     circle / next state     oF skip;F
        <>F     diamond / eventually     <>F true*;F
        vX.F     greatest fixed point     vX.F
        <w>F     weak next     <w>F ~(o(~F))
        []F     square / always     []F vX.(F /\ oX)
        upto     upto     F upto G vX.((F /\ ~G) -> oX)
        F U G     until     F U G
        F W G     unless / weak until     F W G vX.(~G -> (F /\ oX))
        atnext     atnext     F atnext G vX.((G -> F) /\ (~G -> oX))
        leadsto     leadsto     F leadsto G [](F -> <>G)

    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 ...


    References

    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.

  • Many More Identities.