LinDMT: LTL_f Model Checking Modulo Theories

Help

This is a tool for model checking of data-aware dynamic systems modulo theory (DMTs) with respect to certain LTL_f properties, i.e., linear-time properties with a finite-trace semantics.

Input

Example systems can be selected from the dropdown menu. Here we provide a brief description of its components.

DMT

We use a simple json format for DMTs. The json has to specify states, transitions, variables, relations and functions; optionally, also initial facts can be given (e.g., to fix an initial database). The following is an example:

We explain the format and use of the different components.

States

Every state must have an id, an integer; and a name, a string. The names of states can be referred to in the LTL_f formula, see below. One state must in addition have a key initial set to true. At least one state is supposed to have a key final set to true.

Transitions

Each transition must have a source and a target, which are both numbers that correspond to ids of states. In addition, a transition must have a name, a string, which can be referred to in the LTL_f formula, see below. Here the sources and targets of transitions refer to the numeral state ids. Optionally, a transition can have a guard, which is a string that adheres to the following grammar for formulas:

formula ::= (atom) | formula && formula | formula || formula | formula -> formula | (formula) | EXISTS u . formula
atom ::= term == term | term != term | term < term | term <= term | R(term,...,term)
term ::= k | var | term + term | term - term | f(term,...,term)
var ::= v | v' | u

where k is a number, v is the name of a variable of the DMT as specified below, and R and f are names of a relation and a function, respectively, as specified below, with an appropriate number and types of arguments. In a guard, an occurrence of v refers to the current value, i.e., the variable is read; while v' refers to its value in the next state, i.e., the variable is written. Variables u are supposed to be existentially quantified, their name must be of the form _[a-zA-Z]*, i.e., they must start with an underscore.

Parse errors of transition guards occur, in particular, if variables, relations, or functions are not defined; or if relational and functional terms have arguments of inappropriate type.

Variables

Each variable must have a name, a string; a type, also a string, and an initial value. Numeric types for the integers and rationals are predefined, and specified as int or rat. Any other type name that is considered an uninterpreted sort in the SMT sense. If a variable has one of the two numeric sorts, the initial value must be a number, otherwise a string which must match the name of a constant, as defined below.

Relations

Each relation must have a name, a string; and a domain, a list of strings that is considered a list of sorts. Again, int and rat are fixed numeric sorts, while all other sort names are considered uninterpreted.

Functions

Functions are specified in the same way as relations, but in addition they must have a range field. A function whose domain is the empty list is a constant.

Facts

The facts field is optional and of type string, which represents a formula as specified above. However, the formula must be ground, i.e., it may not contain any variables. For convenience, a predicate distinct(term,...,term) as used in SMT is predefined, which is useful to express that constants are supposed to be distinct, e.g. distinct(a,b,c). If such a declaration is missing, constants may be interpreted as the same elements.

Formula

The LTL_f property should adhere to the grammar

psi ::= atom | psi && psi | psi || psi | psi -> psi | X psi | <a> psi | F psi | G psi | psi U psi | (psi) 
atom ::= b | term == term | term != term | term < term | term <= term | R(term,...,term)
term ::= k | v | term + term | term - term f(term,...,term)

where k is a number, v, R, and f are variables, relations, and functions of the DMT, b is the name of a state in the DMT, and a is the name of a transition in the DMT. The temporal operators are X (next), <a> (next via action a) F (future, ◊), and G (globally, ◻).

Functionality

In order to perform model checking, LinDMT constructs

• the constraint graph as a faithful finite-state abstraction of the DMT
• an NFA for the formula ψ
• the product construction of the two

If the latter has a final state, a witness for the given formula is extracted from the product automaton. In the web interface, if the tool succeeds, the tabs below the input fields show the result of the tool. The first tab contains a graphical representation of the DMT. The NFA constructions can be seen in the second tabs, and the product construction in the third. The last tab shows the output, in particular a run witnessing the property ψ, if such a witness exists.