Property Specification

Properties with respect to which parasim computes robustness are specified by the means of STL (Signal Temporal Logic) or STL* (STL with signal value-freeze operator) formulae.

This is a concise tutorial to formula specification. For a computer-scientific definition of STL* see the article "On Expressing and Monitoring Oscillatory Dynamics" by Dluhoš et al.

STL formula is evaluated over a signal, i.e. a sequence of values in time. Therefore, in each point of a signal (at each time point), the formula may be either true or false. The satisfaction of a formula by a signal as a whole is then equal to its value at the start of the signal.

The main feature of STL* is the signal-value freeze operator. This operator enables us to store values and use them to later in comparison with other values. For example the formula *1(G[0,5](x[1]>x)) says "in the future 5 seconds (interval [0,5]), the value of x is lesser than the value of x at this time". The operator *1 stores the value of all variable at given time, x[1] is used to access the stored value (the notation x^*1 is also used, which is, however not very usable in html). The operator G[0,5] says that x[1]>x must hold at all points in the future five seconds.

Values at several different time points may be stored.

Formulae stored in XML files conforming to the following schema. The formula itself is built inductively and enclosed in

<formula xmlns="http://www.sybila.org/parasim/stl-formula">
    <!-- formula itself -->
</formula>

Predicates

Formulae are either predicates or compound formulae (which consist or several formulae). Predicates have the form C1*V1+C2*V2+...+.Cn*Vn>B where C1,...Cn,B are real constants and V1,...,Vn are variables, that is either the variable name (such as x) which signifies the current value of the variable or variable name with index (such as x[i] for i-th stored value) which signifies the stored value for given index.

In XML, the predicate has the following form:

<predicate>
  <variable multiplier="C">X</variable><!-- the current value of X multiplied by C -->
  <variable multiplier="D" frozen="i">X</variable><!-- i-th stored value of X multiplied by D -->
  <greater/><value>V</value><!-- the sum is greater than V -->
</predicate>

Boolean Operators

We may use the following Boolean operators:

• not -- negates the meaning of formula

<not>
  <!-- formula -->
</not>

• and -- both formulae must be true

<and>
  <!-- formula -->
  <!-- formula -->
</and>

• or -- at least one of the formulae must be true

<or>
  <!-- formula -->
  <!-- formula -->
</or>

Temporal Operators

Temporal operators express properties about a time interval, which has to be specified:

<interval>
  <lower type="closed"><!-- start of the interval --></lower>
  <upper type="closed"><!-- end of the interval --></upper>
</interval>

• globally -- the formula must be true during the whole interval

<globally>
  <!-- interval -->
  <!-- formula -->
</globally>

• future -- the formula must be true at leat at one point during the interval

<future>
  <!-- interval -->
  <!-- formula -->
</future>

• until -- the second formula (release) has to be true at some point during the interval. Furthermore, the first formula (condition) has to be true from this point (i.e. not from the start of the interval, when it is not zero) to the point where release is true.

<until>
  <!-- interval -->
  <!-- condition (formula) -->
  <!-- release (formula) -->
</until>