Package ca.uqac.lif.cep.ltl

package ca.uqac.lif.cep.ltl
Processors to express complex patterns over sequences of events with a first-order extension of Linear Temporal Logic called LTL-FO+.

Temporal operators and quantifiers have processors in two versions: Boolean and Troolean.

Boolean processors are called Globally, Eventually Until, Next, and first-order quantifiers. If a0 a1 a2 … is an input trace, the processor Globally produces an output trace b0 b1 b2 … such that bi = false if and only there exists j ≥ i such that bj = false. In other words, the i-th output event is the Boolean verdict of evaluating G φ on the input trace, starting at the i-th event.

Troolean processors are called Always, Sometime, UpTo, After, Every and Some. If a0 a1 a2 … is an input trace, the processor Always produces an output trace b0 b1 b2 … such that bi = false if there exists j ≤ i such that bj = false, and "?" (the "inconclusive" value of LTL3) otherwise. In other words, the i-th output event is the Boolean verdict of evaluating G φ on the input trace, after reading i events.

Author:
Sylvain Hallé
  • Class
    Description
    After
    Troolean implementation of the LTL X operator
    Always
    Troolean implementation of the LTL G operator
    BooleanFirstOrderQuantifier
     
    Eventually
    Boolean implementation of the LTL F processor
    Every
    Troolean implementation of the universal first-order quantifier.
    Exists
    Boolean implementation of the existential first-order quantifier.
    FirstOrderQuantifier
     
    FirstOrderSlice
     
    ForAll
    Boolean implementation of the universal first-order quantifier.
    Globally
    Boolean implementation of the LTL G processor
    HardCast
    Casts a Boolean value into a Troolean value, by converting (Boolean) true into (Troolean) inconclusive.
    Main
    Dummy main file
    NewForAll
     
    NewQuantifier
     
    NewTrooleanForAll
     
    Next
    Boolean implementation of the LTL X processor
    SoftCast
    Casts a Boolean value into a Troolean value, by converting (Boolean) false into (Troolean) inconclusive.
    Some
    Troolean implementation of the existential first-order quantifier.
    Sometime
    Troolean implementation of the LTL F processor
    Troolean
    Implementation of a three-valued logic.
    Troolean.Value
    The three possible values of a Troolean
    TrooleanCast
    Casts an object into a Troolean value
    TrooleanGroundTerm
     
    UnaryOperator
     
    Until
    Boolean implementation of the LTL U processor
    UpTo
    Troolean version of the LTL U operator