Monitoring Arithmetic Temporal Properties

Help

This prototype is a tool to monitor traces over arithmetic variables with respect to LTL_f properties, i.e., linear-time properties with a finite-trace semantics.

Input

Examples can be selected from the dropdown menu. Here we provide a brief description of the input components.

Trace

A trace is given by a non-empty sequence of assignments to a fixed set of data variables V. Each assignment has to mention the same set of variables. In the web interface, every line corresponds to one assignment, which is given as a comma-separated list of variable/value pairs, e.g. specified as x = 12 or temp = 30.3. For instance, the following is a trace:

x = 0, y = 0
x = 1.5, y = 1
x = 2, y = 2
x = 3, y = 1

In this input format, the type of the variables (integer or rational) is simply determined according to whether a value with a decimal point occurs in the list. That is, in this example the set V consists of x, which is assumed rational because of the value 1.5, and y, which is assumed integer. The tool can also be used via the command line (see source code); in this case the trace can be supplied via a json file where the types are fixed explicitly.

Property

The LTL_f property should be expressed as a property with lookahead 1 over the variables V. More precisely, it must adhere to the following grammar:

psi ::= atom | psi && psi | psi || psi | X psi | F psi | G psi | psi U psi | (psi)
atom ::= term == term | term != term | term < term | term <= term | term > term | term >= term
term ::= k | v | v' |  term + term | term - term

where k is a number, v is a data variable in V, and v' refers to the value of v one step ahead. The temporal operators are X (next), F (future, ◊), G (globally, ◻), and U (until).

The following are example properties:

F (x' != x)		There exists a point in the future where the next value of x differs from its current value.
(((x > y + 3) U (x == 100)) && G (x' >= x))		The value of x is greater than that of y+3 until x has value 100, and x is monotonically increasing.

Functionality

The tool monitors the trace against the given LTL_f property, using the approach outlined in the AAAI'23 submission. The tool outputs first the equivalent property with one-step lookback. Next, it is stated whether finite summary was detected or not (if this is not the case, the monitoring procedure need not terminate). It is then determined whether the given trace satisfies the property, and finally what is its monitoring state in the four-valued RV-semantics CS (current satisfaction), PS (permanent satisfaction), CV (current violation), and PV (permanent violation).

In order to determine whether the trace satisfies the property, as well as to build the monitoring structure, the tool constructs first an NFA and then a DFA, which can be viewed in the corresponding tabs of the web interface. If the user issues another request for the same property, the monitoring structures are re-used rather than rebuilt from scratch.

Top