Ada is a tool for model checking of data-aware dynamic systems with arithmetic (DDSAs) with respect to certain LTLf properties, i.e., linear-time properties with a finite-trace semantics.
Example systems can be selected from the dropdown menu. Here we provide a brief description of its components.
Ada uses a simple json format for DDSAs, according to this schema. The json has to specify states, transitions (possibly with guards), and variables, as in the following example:Here the sources and targets of transitions refer to the numeral state ids. The names of states and transitions can be referred to in the LTLf formula, see below. For variables, besides a name also a type (
rat) must be specified, as well as an initial value. Guards in transitions are expected to be formulas written according to the grammar
guard ::= (atom) | guard && guard | (guard) atom ::= term == term | term != term | term < term | term <= term term ::= k | var | term + term | term - term var ::= v | v'where
kis a number, and
vis the name a variable in the DDSA. In a guard, an occurrence of
vrefers 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.
The LTLf formula should adhere to the grammar
psi ::= atom | 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 term ::= k | v | term + term | term - termwhere
kis a number,
vis a variable in the DDSA,
bis the name of a state in the DDSA, and
ais the name of a transition (action) in the DDSA. The temporal operators are
<a>(next via action
F(future, ◊), and
The tool checks several sufficient criteria for finite summary of a DDSA (monotonicity or gap-order constraint system, 2|V|-bounded lookback, and decomposability according to sequential or variable decomposition). If one of these criteria apply, Ada will construct
- the constraint graph as a faithful finite-state abstraction of the DDSA
- an NFA for the formula ψ
- the product construction of the two