Script Syntax

A monitor in MoonLight is specified via a MoonLight script. It supports the specification of properties written with the Reach and Escape Logic (STREL).

1| signal { int nodeType;  real battery;  real temperature; } 
2| space { edges { int hop; real dist; }  } 
3| domain boolean;
4| formula atom = (nodeType==3);
5| formula P1 = atom reach(hop)[0, 1] {(nodeType==1) |  (nodeType==2)};
6| formula Ppar(int k) = atom reach(hop)[0, k] (nodeType== 2);

Script Description

Definition of input signal domains (line 1)

The script (line 1) starts with the definition of the domains of the input signal. We recall that STREL is interpreted over spatio-temporal signals. In our example, these values are:

• the type of node (nodeType)
• the battery level (battery)
• the temperature level (temperature)

As domains, the node type is represented by an integer (int) and the battery and temperature by real values (real).

Definition of Spatial structures domain (line 2)

Spatial structures in STREL can change over time. This enables to model the behaviour of the mobile nodes in our example by updating edges and edge labels. The edges can have more than one label with different domains. In this case, we have two labels: hop having type int domain, and dust with type real. Note that, if one is only interested in temporal properties, this part is omitted in the script.

Definition of monitoring semantics (line 3)

MoonLight, like STREL, supports different semantics for monitoring. A user can specify the desired one by indicating the specific monitoring domain (line 3). Currently, MoonLight supports qualitative (boolean) and quantitative (minmax) semantics of STREL.

Definition of formulas (line 4-6)

After this initial declarations, a script contains the list of formulas that can be monitored (lines 4-6). Formulas can have parameters that are instantiated when monitoring is performed. A formula can be used within another formula.

Syntax of formulas

Formulas are built by using standard Boolean operators:

• negation: !
• conjunction: &
• disjunction: |
• implication: =>

Atomic Expression

An atomic expression consists of Boolean expressions on signal variables

(battery > 0.5) | (nodeType == 2)

As expected, the interpretation of atomic formulas depends on the domain of the monitoring.

Temporal Properties

Temporal properties are specified via the standard until and since operators from which we can derive the future eventually and globally operators and the corresponding past variants, once and historically.

All these operators may take an interval of the form [exp1,exp2] to define where the property should be evaluated. exp1 and exp2 can be algebraic operations. Such an interval can be omitted in the case of unbounded temporal operators.

Examples:

formula phi1 = eventually[1,2](battery > 0.5)
formula phi2 = globally(X > 2)
formula phi3 = once[1,2](battery > 0.5)
formula phi4 = historically[3,4](X > 2)
formula phi5(real a, real b) = historically[3+a,4+a](X > b)

There is also the possibility of define formulas with parameters. Consider for example phi5 where there are 2 real parameters: a and b.

Spatio-temporal Properties

Spatial modalities, instead, are reach and escape operators, and the derivable operators somewhere and everywhere. All these operators may be decorated with a distance expression and a distance interval. The distance expression consists of an expression that is used to compute the length of an edge. If omitted, the real value 1.0 is used. Let us consider the following property

P1 = (nodeType==3)reach(hop)[0, 1]{(nodeType==1)|(nodeType==2)}

P1 holds if from a node of type3 (an end device), we can reach a node of type1 or 2(a coordinator or a router), following a path in the spatial graph such that the hop distance along this path (i.e. its number of edges) is not bigger than 1.

The other operator of STREL, escape, can be used to express the ability to move away from a given point. Let us consider the following property

P2 = escape(hop)[5,inf] (battery > 0.5)

P2 states that from a given location, we can find a path of (hop) length at least 5 such that all nodes along the path have a battery level greater than 0.5 To specify properties around a given location, operators somewhere and everywhere can be used.

P3 = somewhere(dist)[0,300] (battery > 0.5))

P3 is satisfied (at a given location) whenever there is a node at a distance between 0 and 300 having a battery greater than 0.5.

The everywhere operator works in a similar way, however, it requires that its subformula holds in all nodes satisfying the distance constraints.

P4 = everywhere(dist)[0, 10]{eventually[0,5](battery > 0.5)}

P4 holds if each node can reach a node in less than 10 hops where the battery is greater than 0.5 in at least one time step in the next 5 time units.

More details and examples about STREL can be found here.