Ada - the arithmetic DDS analyzer

Help

Ada is a tool for model checking of data-aware dynamic systems with arithmetic (DDSAs) 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.

DDSA

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 LTL_f formula, see below. For variables, besides a name also a type (int or 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 k is a number, and v is the name a variable in the DDSA. 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.

Formula

The LTL_f 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 - term

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

Functionality

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

If the latter was found to have a finite state, Ada moreover extracts a witness for the given formula from the automaton. If Ada succeeds, the tabs below the input fields show the result of th tool. The first tab contains a graphical representation of the DDSA. The three automata constructions can be seen in the next three tabs of the web interface (CG, NFA, PC). The LOG tab shows the output of Ada, including the criteria for finite summary that were found to apply, and a run witnessing the property ψ, in case such a witness exists.

Top