{"id":317,"date":"2012-12-20T14:13:59","date_gmt":"2012-12-20T13:13:59","guid":{"rendered":"https:\/\/project.inria.fr\/plasma-lab\/?page_id=317"},"modified":"2015-08-04T17:18:59","modified_gmt":"2015-08-04T15:18:59","slug":"property-language","status":"publish","type":"page","link":"https:\/\/project.inria.fr\/plasma-lab\/documentation\/languages\/property-language\/","title":{"rendered":"Bounded Linear Temporal Logic"},"content":{"rendered":"

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

Any decidable property on states or runs can be used in the formulas including nested B-LTL operators.<\/p>\n

Thus, the semantic of our B-LTL logic is the semantic of LTL logic restricted to a time interval.<\/p>\n

Important!<\/strong><\/p><\/p>\n

For a quick introduction to LTL you could read the wikipedia article on Linear Temporal Logic<\/a><\/strong>.<\/p>\n

<\/div>\n

\n

B-LTL Grammar<\/h3>\n

The grammar accepted by our BLTL plugin is the following:<\/p>\n

Property ::= ( ('declare' Variable (';' Variable)*)?\r\n               ('optimize' Variable (';' Variable)*)?\r\n               'end')? Formula\r\nFormula ::= 'F <=' Bound Formula\r\n    | 'G <=' Bound Formula\r\n    | Formula 'U <=' Bound Formula\r\n    | Formula 'W <=' Bound Formula\r\n    | 'X' ('<=' Bound)? Formula      \r\n    | Formula '&' Formula\r\n    | Formula '|' Formula\r\n    | Formula '=>' Formula\r\n    | '!' Formula\r\n    | '(' Formula ')'\r\n    | 'true'\r\n    | 'false'\r\n    | Numerical Operator Numerical\r\nBound ::= ('#')? Numerical\r\nVariable ::= ident ':=' (Interval | number)\r\nInterval ::= '['number';'number';'number']'\r\nNumerical ::= ident | number\r\nOperator ::=  '<' | '<' | '!=' | '=' | '>=' | '>' | '+' | '-' | '*' | '\/' \r\n<\/pre>\n
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.\n\n\n\n
Optimisation<\/h3>\n
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:
\n
Important!<\/strong><\/p>declare K:=[5;10;5] end
\nF<=#(K) “eat”<\/div>
\ngenerates a property whose temporal bound is successively 5 and 10.<\/p>\n
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:
\n
Important!<\/strong><\/p>optimize p1:=[0;5;1]  end
\nF<=#5 “eat”<\/div>
\nwill check the property for each values of the variable p1 from 0 to 5 with an increment of 1.<\/p>\n
For more information look at the tutorial on optimisation<\/a><\/strong>.<\/p>\n
\n
Nested B-LTL<\/h3>\n
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:<\/p>\n
Property::=\r\n    'Pr >=' number '['Property']'<\/pre>\n
\n
Adaptive BLTL (A-BLTL)<\/h3>\n
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:<\/p>\n
Property ::= ( ('declare' Variable (';' Variable)*)?\r\n               ('optimize' Variable (';' Variable)*)?\r\n               'end')? Formula\r\nFormula ::= BLTL_Formula\r\n    | BLTL_Formula '; [' Trigger ',' Trigger '] ==>' Formula\r\n    | BLTL_Formula '; [' Trigger ',' Trigger '] <=' Bound '==>' Formula\r\n    | BLTL_Formula '==> [' Trigger ',' Trigger '] ;' Formula\r\n    | BLTL_Formula_Formula '==> [' Trigger ',' Trigger '] <=' Bound ';' Formula Trigger ::=      Trigger '=>' Trigger\r\n    | Trigger '&' Trigger\r\n    | '!' Trigger\r\n    | '(' Trigger ')'\r\n    | 'true'\r\n    | 'false'\r\n    | Numerical Operator Numerical\r\nBound ::= ('#')? Numerical\r\nVariable ::= ident ':=' (Interval | number)\r\nInterval ::= '['number';'number';'number']'\r\nNumerical ::=  ident | ident \"'\" | number\r\nOperator ::=  '<' | '<' | '!=' | '=' | '>=' | '>' | '+' | '-' | '*' | '\/' <\/pre>\n
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:<\/p>\n