LTL Model Checking

ProB provides support for LTL (linear temporal logic) model checking. For an introduction see the Wikipedia Article.

To use this feature, select "Check LTL formula..." in the "Verify" menu. The following dialog appears:

You can enter an LTL formula in the dialog's text field. We explain the supported syntax below. If the model checker finds a counter-example the animator navigates to the last state of the counter-example. The full path can then be seen in the history.

Search options

The model checker searches for a counter-example (i.e. a path that does not satisfy the current formula). Where the checked pathes through the model's search space start depend on the following options:

1. Start search in initialisation
   All pathes that start in a state of the initialisation of the machine are checked.
2. Start search in current state
   All pathes that start in the current state are checked.
3. Start in initialisation, but check formula in current state
   All pathes that start in a state of the initialisation of the machine are checked, but the formula is mapped to the current state. E.g., this option can be used to check properties like "Is this state only reachable directly after executing operation `xy`?": The formula would be `Y[xy]`. This is equivalent to "G (current => f)" with f as the entered formula and using option "Start search in initialisation".

Note: Whereas `Y true` is always false when checked with option 1 or 2, it is usually true (but not in all cases) for option 3.

Search results

There are three possible results:

• The formula is true for all valid pathes.
• There is a path that does not satisfy the formula. This counter-example is shown in the history of the animator.
• No counter-example was found, but the absence of a path that does not satisfy the formula can not be guaranteed because the state space was not fully explored.

Exploring new states

The LTL model checker searches in the already explored search space of the model. If a state is encountered that has not been explored before, the state will be explored (i.e. all transitions to successor states are calculated). The number of how often this can happen is limited by the field "Max no. of new states".

Depending on the LTL formula, a partially explored state space can be sufficient to find a counter-example or to assure the absence of a counter-example. If there's still the possibility of a counter-example in the remaining unexplored state space, the user will get a message.

Supported Syntax

ProB supports LTL^e, an extended version of LTL. In contrast to standard LTL, LTL^e also supports propositions on transitions, not only on states. In practice, this allows the operator `[...]` (see below). Also Past-LTL is supported.

• Atomic propositions can be one of the following:
  • predicates can be written in curly braces: `{...}`. E.g. `{card(someset) > 1}`
  • To check if an operation is enabled in a state, `e(Op)` can be used, where `Op` is the name of the operation.
  • If a state is the current state in the animation can be checked with `current`.
  • If there is no operation that lead to a different state, can be checked with `sink`. This can be useful to find "pseudo"-deadlocks, where only query-operations are enabled, that do not change the state.
  • Whether a state is a deadlock state can be checked with `deadlock`.

• Transition propositions:
  If the next executed operation in the path is `Op`, the expression `[Op]` can be used. Also patter-matching for the arguments of the operation is supported. E.g. `[Op(3,,4*v)]` checks if the next operation is `Op` and that the first argument is 3 and the third argument is `4*v` where `v` is a variable of the machine.
  Arbitrary B expressions can be used as patterns. Constants and variables of the machine can be used, variables have the values of the state where the operations starts.

• Logical operators
  • `true` and `false`
  • `not`: negation
  • &, `or` and =>: conjunction, disjunction and implication

• Temporal operators (future)
  • `G f`: globally
  • `F f`: finally
  • `X f`: next
  • `f U g`: until
  • `f W g`: weak until
  • `f R g`: release

• Temporal operators (past)
  • `H f`: history (dual to G)
  • `O f`: once (dual to F)
  • `Y f`: yesterday (dual to X)
  • `f S g`: since (dual to until)
  • `f T g`: trigger (dual to release)

LTL assertions in the definitions clause

LTL formulas can be stored in the `DEFINITIONS` section of a B machine. The name of the definition must start with `ASSERT_LTL` and a string must be specified. E.g.:

DEFINITIONS
 ASSERT_LTL == "G ([add] => X {card(db)>0})"

All assertions can be checked automatically by selecting "Check LTL assertions" in the "Verify" menu. Each formula is checked for all paths starting in the states of the initialisation of the machine. Formulas that pass are marked green, formulas that failed are marked red.

LTL formulas in a separate file

With the command line version of ProB it is possible to check several LTL formulas with one call. The command has the following syntax

probcli -ltlfile FILE ...

The file FILE contains one or more sections, where each section has the form

[Name]
 Formula

The formula itself can spread several lines. Additional comments can be added with a leading #.

If a counter-example is found, the trace of the counter-example is saved into the file

ltlce_Name.trace

, where Name is the name of the formula in the LTL file.