Ada - the arithmetic DDS analyzer


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 (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.


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 - 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, ◻).


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

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.