Breach temporal logic formulas

Author       Home       Download and install       Systems       Simulation       Temporal Logic       Parameter sets       Graphical User Interfaces      

A feature of Breach which makes it different (if not unique) from standard ODE or hybrid systems simulators is the ability to define temporal logic formulas and check whether they are satisfied by simulated trajectories. Moreover it provides a boolean as well as a quantitative satisfaction information. Let us call \(\xi\) a simulation trace and \(\varphi\) a formula. Breach computes a function \(\tau \rightarrow \rho(\varphi, \xi, \tau)\) such that

\(\xi\) satisfies \(\varphi\) at time \(\tau\), noted \(\xi, \tau\ \models \varphi\) if and only if \(\rho(\varphi,\xi, \tau)>0\)

In Breach, formulas are implemented within the class QMITL_Formula. A new formula is created either by using the 'New' button of the properties panel of the main GUI, or by using the QMITL_Formula constructor. In both cases, the user has to supply an id and a string which defines the formula. A command line call to the constructor looks like this:

>> QMITL_Formula('phi', 'ev (x0[t]>1)');

It will create in the Matlab workspace a new variable of type QMITL_Formula named phi. The string given as second argument must describe a valid formula in Signal Temporal Logic (STL), which we describe in the next section. Also, examples are given in this page. Alternatively, formulas can be defined in a file, e.g.:


# everything starting with # is a a comment
# let's define a few predicates
p1 := x0[t]>1
p2 := x1[t] + 2*x2[t] < 1

# Formulas can reuse previously defined formulas or predicates
phi1 := p1 and p2

# Formulas can be written on several lines
phi2 := alw (p1 => 
                   ev  ( p1 or p2 )

and loaded in Matlab workspace using QMITL_ReadFile:

>> formulas = QMITL_ReadFile('formulas.stl');

Vizualizing property satisfaction in the GUI

If a formula \(\varphi\) appears in the properties panel of the main GUI when the trajectories GUI is invoked, then it will appear in the trajectories GUI as well, meaning that you can select it instead of a variable as the y-axis of any of the three axes. In this case, Breach will compute the satisfaction function for this formula and for the current trajectories for all time for which this trajectory has been computed. The quantitative satisfaction function is plotted in blue and the Boolean satisfaction function is normalized (with False = 0 and True = \(max(|\rho|)/2\) ) and plotted in red, see the figure below as a first example :


Signal Temporal Logic (STL)

An STL formula \(\varphi\) can be constructed with the following grammar: $$ \varphi := \mu \ |\ \neg \varphi\ |\ \varphi \wedge \varphi\ |\ \varphi \vee \varphi |\ \varphi\ \mathcal{U}_{[a,b)}\ \varphi\ |\ ev_{[a,b)}\ \varphi\ |\ alw_{[a,b)}\ \varphi $$ where

  • \(\mu\) is a base predicate;
  • \(\neg\), \(\wedge\), and \(\vee\) are standards Boolean operators;
  • \(\mathcal{U}\), \(ev\) and \(alw\) are temporal operators.

In the following we explain how to declare predicates and then how to compose them using the Boolean and temporal operators.

Writing predicates

A predicate \(\mu\) within Breach is a general inequality relation on the variables and the parameters of the system under study. E.g. assume that we are working with the Lorenz dynamical system defined in the documentation on systems creation. This system has variables \(x_0[t]\), \(x_1[t]\), \(x_2[t]\) and parameters \(x_0, x_1, x_2, a, b, f, g\) where the 3 first parameters are initial conditions for the variables, i.e.,

\(x_0 = x_0[t]_{|t=0}\), \(x_1 = x_1[t]_{|t=0}\) and \(x_2 = x_2[t]_{|t=0}\).

For this system, a trace \(\xi\) is a function from \( t \) to \(\mathbb{R}^3\): \(\xi[t] = (x_0[t], x_1[t], x_2[t])\). A predicate for this system is thus an inequality involving these variables and parameters. Here are simple examples :

  • \(\mu_1 := x_0[t] > 0\)
  • \(\mu_2 := x_0[t] + 2x_1[t] > 0\)
  • \(\mu_3 := bx_0[t]x_1[t] + x_0[t]x_2[t] < x_2[t]\)

Note: Breach does not make a difference between strict and non-strict inequalities.

Since a predicate is an inequality constraint on a function of \( t \), Breach interprets it by computing the residual of this inequality. Obviously, the sign of this residual provides the Boolean satisfaction of the predicate and the residual itself provides the quantitative satisfaction. More precisely, Breach first transforms the predicate \(\mu\) into a canonical form \(\tilde{\mu}(\xi,t) > 0\) by substracting the right-hand side of \(\mu\) to the left-hand side and swapping the comparison operator if necessary. The function (residual) \(\tilde{\mu}\) is used for the satisfaction function.

For the examples above, it gives:

  • \(\rho(\mu_1,\xi, t) = \tilde{\mu}_1(\xi,t) = x_0[t]\), Example plot
  • \(\rho(\mu_2,\xi, t) = \tilde{\mu}_2(\xi,t) = x_0[t] + 2x_1[t]\), Example plot
  • \(\rho(\mu_3,\xi, t) = \tilde{\mu}_3(\xi,t) = x_2[t] - bx_0[t]x_1[t] - x_0[t]x_2[t]\), Example plot

Note that there is no normalization in the computation of \(\tilde{\mu}\) from \(\mu\), so that, e.g., \(\mu_1 := x_0[t] > 0\) is interpreted differently from \(\mu_1' := 2x_0[t] >0\).

More on predicates: Breach is quite flexible in the definition of predicates. Arbitrary complex symbolic expressions can be used, involving any mathematical function that Matlab knows. Additionally, since \(\xi\) is obtained from an ODE solver with a forward sensitivity analysis capability, Breach has access to the time derivatives of the variables as well as their derivatives with respect to parameters. See the formula bestiary.

Boolean operators

Boolean operators are interpreted as usual for the Boolean satisfaction of formulas. For the quantitative satisfaction, the negation is simply the opposite and conjunction and disjunction are interpreted through the classical min-max correspondance, i.e.,

  • \(\rho(\neg \varphi, \xi, t) = - \rho(\varphi, \xi,t)\) Example plot
  • \(\rho(\varphi_1 \vee \varphi_2, \xi, t) = \max (\rho(\varphi_1, \xi,t), \rho(\varphi_2, \xi,t))\) Example plot
  • \(\rho(\varphi_1 \wedge \varphi_2, \xi, t) = \min (\rho(\varphi_1,\xi,t), \rho(\varphi_2,\xi,t))\) Example plot

Temporal operators

The temporal operators makes it possible to characterize the satisfaction of subformulas at different time instants.

The \(ev\) (eventually) operator checks wether a formula is satisfied at some time in a future interval of the form \([t+a, t+b)\) where \( a \) can be 0 and \( b \) can be \(\infty\). Formally, the Boolean satisfaction is given by : $$ (\xi, \tau) \models ev_{[a,b)} \varphi \Leftrightarrow \exists \tau' \in [\tau +a,\tau +b)\ \text{such that}\ (\xi,\tau') \models \varphi $$

The quantitative satisfaction function is given by the maximum satisfaction of the subformula over the (moving) interval \([t+a, t+b)\): $$ \rho(ev_{[a,b)} \varphi,\xi,\tau ) = \displaystyle \sup_{\tau' \in [\tau +a,\tau +b)} \rho(\varphi, \xi, \tau') $$

Here are two examples :

  • Unbounded eventually (\(a=0\) and \(b=\infty\)): \(\varphi_1 = ev\ \mu_3\) Example plot
  • Bounded eventually (\(a=0.5\) and \(b=1.5\)) \(\varphi_2 = ev_{[0.5, 1.5)}\ \mu_3\) Example plot

The \(alw\) (always) operator checks wether a formula is satisfied at all time in a future interval of the form \([t+a, t+b)\) where \( a \) can be 0 and \( b \) can be \(\infty\). Formally, the Boolean satisfaction is given by : $$ (\xi, \tau) \models alw_{[a,b)} \varphi \Leftrightarrow \forall \tau' \in [\tau +a, \tau +b),\ (\xi,\tau') \models \varphi $$ Here are two examples :

  • Unbounded always (\(a=0\) and \(b=\infty\)): \(\varphi_3 = alw\ \mu_3\) Example plot
  • Bounded always (\(a=0.5\) and \(b=1.5\)) \(\varphi_4= alw_{[0.5, 1.5)}\ \mu_3\) Example plot

The \(\mathcal{U}\) (Until) operator is a binary operator which is satisfied when its fist formula argument is continuously true until its second formula argument is true at some time in a future interval of the form \([t+a, t+b)\) where \( a \) can be 0 and \( b \) can be \(\infty\). Formally, the Boolean satisfaction is given by : $$ (\xi,\tau)\models \varphi_1 \mathcal{U}_{[a,b)} \varphi_2\ \Leftrightarrow\ \exists \tau' \in [\tau+a, \tau+b)\ \text{such that}\ (\xi,\tau') \models \varphi_2 \text{ and }\ \forall \tau'' \in [\tau, \tau'),\ (\xi,\tau'') \models \varphi_1 $$

Here is one example : \( \varphi_5 = (x_0[t]<1)\ \mathcal{U}_{[a,b)}\ (x1[t]>1)\ \) Example plot