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