Bounded Linear Temporal Logic

Our property logic is based on a Bounded Linear Temporal Logic (B-LTL). This logic enhance Linear Temporal Logic (LTL) operators with bounds expressed in step or time units. These bounds gives the length of the run on which the nested formula must hold.

Any decidable property on states or runs can be used in the formulas including nested B-LTL operators.

Thus, the semantic of our B-LTL logic is the semantic of LTL logic restricted to a time interval.

B-LTL Grammar

The grammar accepted by our BLTL plugin is the following:

Property ::= ( ('declare' Variable (';' Variable)*)?
               ('optimize' Variable (';' Variable)*)?
               'end')? Formula
Formula ::= 'F <=' Bound Formula
    | 'G <=' Bound Formula
    | Formula 'U <=' Bound Formula
    | Formula 'W <=' Bound Formula
    | 'X' ('<=' Bound)? Formula      
    | Formula '&' Formula
    | Formula '|' Formula
    | Formula '=>' Formula
    | '!' Formula
    | '(' Formula ')'
    | 'true'
    | 'false'
    | Numerical Operator Numerical
Bound ::= ('#')? Numerical
Variable ::= ident ':=' (Interval | number)
Interval ::= '['number';'number';'number']'
Numerical ::= ident | number
Operator ::=  '<' | '<' | '!=' | '=' | '>=' | '>' | '+' | '-' | '*' | '/'

The difference with classical Linear Temporal Logic is that temporal operators (F, G, X, U and W) are bounded by a temporal bound. This bound may either be a number of steps (using the syntax <= # Numerical) or a real-time bound (using the syntax <= Numerical). If the model is untimed, the two syntax are equivalent.

Optimisation

It is possible to declare a new variable in a BLTL property and assign a range of values to it. This generates a set of BLTL formulas that can be checked simultaneously by some SMC algorithms. For instance:


generates a property whose temporal bound is successively 5 and 10.

It is also possible to optimize existing variables in the model and assign similarly a range of initial values to it. When checking such a property several initial states will be successively checked by the SMC algorithm.For instance:


will check the property for each values of the variable p1 from 0 to 5 with an increment of 1.

For more information look at the tutorial on optimisation.

Nested B-LTL

We added a new “nested probability” operator. This operator allows you to check, within a property, if a sub-property’s probability is superior or equal to a given probability. To do this we extended the B-LTL grammar with a new nested transition:

Property::=
    'Pr >=' number '['Property']'

Adaptive BLTL (A-BLTL)

We have extended the grammar of BLTL with two adaptive operators that observe adaptive transitions in stochastic adaptive systems (SAS). The grammar of the new logic is the following:

Property ::= ( ('declare' Variable (';' Variable)*)?
               ('optimize' Variable (';' Variable)*)?
               'end')? Formula
Formula ::= BLTL_Formula
    | BLTL_Formula '; [' Trigger ',' Trigger '] ==>' Formula
    | BLTL_Formula '; [' Trigger ',' Trigger '] <=' Bound '==>' Formula
    | BLTL_Formula '==> [' Trigger ',' Trigger '] ;' Formula
    | BLTL_Formula_Formula '==> [' Trigger ',' Trigger '] <=' Bound ';' Formula Trigger ::=      Trigger '=>' Trigger
    | Trigger '&' Trigger
    | '!' Trigger
    | '(' Trigger ')'
    | 'true'
    | 'false'
    | Numerical Operator Numerical
Bound ::= ('#')? Numerical
Variable ::= ident ':=' (Interval | number)
Interval ::= '['number';'number';'number']'
Numerical ::=  ident | ident "'" | number
Operator ::=  '<' | '<' | '!=' | '=' | '>=' | '>' | '+' | '-' | '*' | '/'

As presented above, the two adaptive operators of A-BLTL can be either bounded or unbounded. Informally the semantics of these operators is the following:

  • BLTL Property ‘==> [‘ Trigger ‘,’ Trigger ‘] ;’ Property, is satisfied by an execution if the first BLTL property is satisfied by the first state and there exists an adaptive transition that satisfies the tiggers and the second property is satisfied by the state reached just after the adaptive transition.
  • BLTL Property ‘; [‘ Trigger ‘,’ Trigger ‘] ==>’ Property, is satisfied by an execution if when the first BLTL property is satisfied by the first state and there exists an adaptive transition that satisfies the tiggers, then the second property is satisfied by the state reached just after the adaptive transition. Therefore in this semantics it is not necessary to observe an adaptive transition in order to satisfy the property.

The triggers are Boolean expressions over the variables of the model. The first trigger is evaluated on the state just before an adaptive transition, while the second is evaluated on the state reached just after the adaptive transition. To specifiy expressions, A-BLTL include an additional prime operator on identifiers that test if a variable exists and returns false in the contrary.

Comments are closed.