A Filtered Oscillator

We consider a filtered oscillator model adapted from [1]. The filtered oscillator consists of a $2$-dimensional switched oscillator of signals $x$ and $y$ with a $k$-series of first-order filters. The filters smoothens an input signal $x$, producing an output signal $z$. When the signal $x$ goes through each filter, the amplitude of the signal diminishes as it passing by. Each filter $i \in \{0, 1, 2, 3\}$ takes an input signal $x_i$ and outputs a diminished signal $x_{i + 1}$, where $x_0 = x$ and $x_4 = z$.

Figure [1] shows a hybrid automaton of the filtered oscillator. Initially, the $x$ and $y$ are in $[0.2, 0.3]$ and $[-0.1, 0.1]$, respectively and all filters output zero signals. The jumps between modes define the behavior of the filtered oscillator to maintain a stable oscillation.

Fig.1: A hybrid automaton of the filtered oscillator

Table [1] shows the STL properties.

Label	STL formula	Description
$\textsf{f1}$	$\lozenge_{[0,3]} ((x_3 \geq 1) \mathbf{R}_{[0, \infty)} (y \leq 10))$	For some time point in $[0, 3]$, $y$ is less than or equal to $10$, until $x_3$ is greater than or equal to $1$ within time interval $[0, \infty)$.
$\textsf{f2}$	$\lozenge_{[2,5]} (\square_{[0,3]} (x_2 < 4))$	For some time point in $[2, 5]$, $x_2$ is always less than $4$ during $3$ time units.
$\textsf{f3}$	$(\square_{[1,3]} (x \leq 2)) \mathbf{R}_{[2,5]} (x_3 > 2)$	For time interval $[2, 5]$, $x_3$ is greater than $2$, until $x$ is less than or equal to $2$ within time interval $[1, 3]$.

Table.1: STL properties for the filtered oscillator

---

An STLmc Input Model

We use the STLmc language to describe the filtered oscillator model (oscillator.model) as follows:

real loc;
[-100, 100] x;  [-100, 100] y;  [-100, 100] z;
[-100, 100] x1; [-100, 100] x2; [-100, 100] x3;
{ mode: loc = 1;
  inv:  x >= 0;
        y + 2 * x >= 0;
  flow: d/dt[x] = -0.2 * x + 1.4; 
        d/dt[y] = -0.1 * y - 0.7;
        d/dt[x1] = 3 * x - 3 * x1;
        d/dt[x2] = 3 * x1 - 3 * x2;
        d/dt[x3] = 3 * x2 - 3 * x3;
        d/dt[z] = 3 * x3 - 3 * z; 
  jump: (and (x >= 0) (y + 2 * x <= 0)) => 
        (and (loc' = 2) (x' = x) (y' = y) 
             (x1' = x1) (x2' = x2) (x3' = x3)
             (z' = z));
}
{ mode: loc = 2;
  inv:  x >= 0;
        y + 2 * x <= 0;
  flow: d/dt[x] = -0.2 * x - 1.4;
        d/dt[y] = -0.1 * y + 0.7;
        d/dt[x1] = 3 * x - 3 * x1;
        d/dt[x2] = 3 * x1 - 3 * x2;
        d/dt[x3] = 3 * x2 - 3 * x3;
        d/dt[z] = 3 * x3 - 3 * z; 
  jump: (and (x <= 0) (y + 2 * x <= 0)) =>
        (and (loc' = 3) (x' = x) (y' = y)
             (x1' = x1) (x2' = x2) (x3' = x3)
             (z' = z));
}
{ mode: loc = 3;
  inv:  x <= 0;
        y + 2 * x <= 0;
  flow: d/dt[x] = -0.2 * x - 1.4;
        d/dt[y] = -0.1 * y + 0.7;
        d/dt[x1] = 3 * x - 3 * x1;
        d/dt[x2] = 3 * x1 - 3 * x2;
        d/dt[x3] = 3 * x2 - 3 * x3;
        d/dt[z] = 3 * x3 - 3 * z;
  jump: (and (x <= 0) (y + 2 * x >= 0)) =>
        (and (loc' = 4) (x' = x) (y' = y)
             (x1' = x1) (x2' = x2) (x3' = x3)
             (z' = z));
}
{ mode: loc = 4;
  inv:  x <= 0;
        y + 2 * x >= 0;
  flow: d/dt[x] = -0.2 * x + 1.4;
        d/dt[y] = -0.1 * y - 0.7;
        d/dt[x1] = 3 * x - 3 * x1;
        d/dt[x2] = 3 * x1 - 3 * x2;
        d/dt[x3] = 3 * x2 - 3 * x3;
        d/dt[z] = 3 * x3 - 3 * z;
  jump: (and (x >= 0) (y + 2 * x >= 0)) =>
        (and (loc' = 1) (x' = x) (y' = y)
             (x1' = x1) (x2' = x2) (x3' = x3)
             (z' = z));
}
init: loc = 1; 0.2 <= x; x <= 0.3; 
              -0.1 <= y; y <= 0.1;
      x1 = 0; x2 = 0; x3 = 0; z = 0; 


proposition:

# bound: 5, timebound: 8, solver: dreal
goal:
  [f1]: <>[0,3]((x3 >= 1) R[0, inf) (y <= 10)); # threshold: 0.1, time-horizon: 2
  [f2]: <>[2, 5] ([][0, 3] (x2 < 4));		# threshold: 1.0, time-horizon: 2
  [f3]: ([][1, 3] (x <= 2)) R[2, 5] (x3 > 2); 	# threshold: 0.1, time-horizon: 2

---

Run

For the input model, we use a time bound $\tau = 8$ and a discrete bound $N = 5$ as input parameters. Because the model has nonlinear dynamics, we use $\textsf{dReal}$ for an underlying solver with the algorithm $\textsf{2-step}$. For efficient model checking, we also use the $\textsf{parallel}$ option. For the formulas $\textsf{f1}$, $\textsf{f2}$, and $\textsf{f3}$, we choose thresholds $\epsilon_1 = 0.1$, $\epsilon_2 = 1.0$, and $\epsilon_3 = 0.1$, respectively.

STLmc finds counterexamples for $\textsf{f2}$ and $\textsf{f3}$, while $\textsf{f1}$ is safe. The following shows the command finding a counterexample for the STL formula $\textsf{f2}: \Diamond_{[2,5]} (\square_{[0,3]} (x_2 < 4))$ at bound $3$ with respect to $\epsilon_2=1.0$ in $8$ seconds using dReal.

./stlmc ./oscillator.model -bound 5 -time-bound 8 -threshold 1.0 \
        -goal f2 -solver dreal -two-step -parallel -time-horizon 2 -visualize

Label	$\epsilon$	$| \Psi |$	Time	Result	$k$	Alg.	#$\pi$
$\textsf{f1}$	$0.1$	$1.5$	$110$	$\top$	-	$\textsf{2-step}$	$289$
$\textsf{f2}$	$1.0$	$1.2$	$224$	$\bot$	$3$	$\textsf{2-step}$	$259$
$\textsf{f3}$	$0.1$	$1.2$	$266$	$\bot$	$3$	$\textsf{2-step}$	$266$

Table.2: Verification results of the STL properties for the filtered oscillator

---

Visualization

Fig.2: Visualization of a counterexample (a horizontal dotted line denotes $\epsilon = 1.0$)

Figure [2] shows the visualization graphs for $\textsf{f2} = \lozenge_{[2, 5]} (\square_{[0, 3]} \, x_2 < 4)$ with the subformulas:

\begin{align*} \textsf{f2}_{\textsf{1}} = \square_{[0, 3]} \, x_2 < 4 \qquad \textsf{f2}_{\textsf{2}} = x_2 < 4 \end{align*}

The robustness degree of $\textsf{f2}$ is less than $\epsilon$ at time $0$, since the robustness degrees of $\textsf{f2}_{\textsf{1}}$ is always less than $\epsilon$ in the interval $[2, 5]$, which is because the degree of $\textsf{f2}_{\textsf{2}}$ goes below $\epsilon$ in $[2, 8] = [2, 5] + [0, 3]$.

---

Reference

[1]. Frehse G. et al. (2011) SpaceEx: Scalable Verification of Hybrid Systems. In: Gopalakrishnan G., Qadeer S. (eds) Computer Aided Verification. CAV 2011. Lecture Notes in Computer Science, vol 6806. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-22110-1_30