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_{[0,0.25]}(x\leq0.2))\mathbf{R}_{[0,0.5]}(x_3>2)$ | The release condition relates $x_3>2$ over $[0,0.5]$ to the nested always condition $x\leq0.2$ over the relative interval $[0,0.25]$. |
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]: ([][0, 0.25] (x <= 0.2)) R[0, 0.5] (x3 > 2); # threshold: 0.1, time-horizon: 2
Run
The following settings and example measurements use STLmc. A counterexample is a trace below the specified robustness threshold; a satisfied result applies only to the bounds shown. Timings vary by machine.
stlmc ./oscillator.model -bound 5 -time-bound 8 -threshold 4 -goal f2 -solver dreal -time-horizon 8 -visualize -path-strategy explicit -ode-order 10 -smt-preprocess
| Goal | Max bound | Time bound | Time horizon | Threshold | Solver | Engine | Seconds | Result |
|---|---|---|---|---|---|---|---|---|
f1 |
1 | 8 | 8 | 0.1 | dreal | one-step | 27.518 | satisfied up to bound 1 |
f2 |
5 | 8 | 8 | 4 | dreal | one-step | 12.997 | violated at bound 0 |
f3 |
5 | 1 | 1 | 0.1 | dreal | one-step | 5.837 | violated at bound 0 |
Select -goal, -bound, -time-bound, -time-horizon, and -threshold
according to the row.
Visualization
The plot shows the f2 counterexample for oscillator.model
with the settings above. Its sampled robustness is compared with the threshold.
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