Slides @ mjvc.me/RV2018
\(\star\): University of California-Berkeley
\(\dagger\): University of Southern California
Survey: Li, Wenchao. Specification mining: New formalisms, algorithms and applications.
$^1$Vazquez-Chanlatte et al, Logic-based Clustering and Learning for Time-Series Data, CAV 2017
$^2$ Bombara et al., Signal Clustering Using Temporal Logics, RV 2017.
This talk is about unifying these two.
\(^*\)Logical Lens = A Parametrized family of Boolean Properties, \(\phi : \text{Parameter} \to \big (\text{Data} \to \{0, 1\}\big )\), e.g. PSTL.
Logical Lens \(\triangleq\) Parametric Trace Property
Goal: Detect highway slow downs.
Have rough idea of shapes to look for.
Logical Lens \(\triangleq\) Parametric Trace Property
\[\phi(\tau, h) \triangleq \square_{[\tau, 20]}(\text{car_speed} \leq h)\]
Different parameters result in different classifications.
If two things are logically similar, they should be "close" together.
If two things are logically similar, they should be "close" together.
"If it quacks like a duck and looks like a duck\(\ldots \) it should have a small distance to a duck."
Time-Series using PSTL is just an example
\[\varphi_i : \text{Data} \to \{0, 1\}\]
Each axis represents a property.
You must be $h$ meters tall or more to ride.
\[\phi : \text{Height} \to \bigg ( \text{Data} \to \{0, 1\}\bigg)\]
\[\phi : \text{Data} \to \bigg ( \text{Height} \to \{0, 1\}\bigg)\]
\[\phi : \text{Data} \to \bigg ( {[0, 1]}^n \to \{0, 1\}\bigg)\]
Data induces a geometric structure in the parameter space.
\[\phi : \text{Data} \to \bigg ( {[0, 1]}^n \to \{0, 1\}\bigg)\]
\[\theta \leq \theta' \implies \phi(x)(\theta) \leq \phi(x)(\theta')\]
It is sufficent to just remember the boundary (surface)
Map Data to Surfaces.
CAV 2017 work can only pick out a single point.
Does similar data induce a similar structure??
"If it quacks like a duck and looks like a duck\(\ldots \) it should produce a similar validity domain boundary??"
Does similar data induce a similar structure??
It depends...
For many Monotonic Specifications this is true: \[ \big( x \geq \theta\big ) \text{ vs } \big(x + 0.1 \geq \theta\big) \]
Logical Lens \(\triangleq\) Parametric Trace Property
Technique due to Oded Maler.
Oded Maler. Learning Monotone Partitions of Partially-Ordered Domains 2017. ă€ˆhal-01556243ă€‰
Steady state error example
Logical Lens \(\triangleq\) Parametric Trace Property
Colyar, J., Halkias, J.: US highway 101 dataset. Federal Highway Administration (FHWA), Tech. Rep. FHWA-HRT-07-030 (2007)
Compute intersections along a line.
Parameterize line between 0 and 1.
\(\gamma_i : \text{Data} \to [0, 1]\).
Can project to multiple lines.
Logical Lens \(\triangleq\) Parametric Trace Property
Zoom in on cluster 4 by computing distances to idealized slow down.
Labels \(\to\) Parameter Ranges \(\to\) Formula
Details in the CAV 2017 paper.
Logic-based Clustering and Learning for Time-Series Data, CAV 2017
\[ \phi(\tau, h) \triangleq \square_{[\tau, 20]}(\text{car_speed} < h) \]
\[ \psi_1 = \phi(0.25, 0.55) \wedge \neg \phi(0.38, 0.55) \wedge \neg \phi(0.25, 0.76) \]
\[ \psi_2 = \phi(0.35, 0.17) \wedge \neg \phi(0.35, 0.31) \wedge \neg \phi(0.62, 0.17) \]
\[\text{slow_down} \triangleq \psi_1 \wedge \psi_2\]
Slides @ mjvc.me/RV2018
- Andrew Ng,"Coming up with features is difficult, time-consuming, requires expert knowledge. "Applied machine learning" is basically feature engineering."
- Pedro Domingos," â€¦some machine learning projects succeed and some fail. What makes the difference? Easily the most important factor is the features used."
... or at least is was before Deep Learning
This work focuses on try to make designing features slightly less hard (e.g., time series).
\[\phi : \text{Data} \to \bigg ( {[0, 1]}^n \to \{0, 1\}\bigg)\]
\[V_\phi(x) \triangleq ~\text{preImg}_{\phi(x)}[\{1\}] = \{\theta \in {[0, 1]}^n~.~\phi(x)(\theta) = 1\}\]
(3/5) Derive a "logical distance" under this lens.
\[\phi(\tau, h) \triangleq \square_{[\tau, 20]}(\text{car_speed} \leq h)\]
(4/5) Apply to real highway data.
\[\phi(\tau, h) \triangleq \square_{[\tau, 20]}(\text{car_speed} \leq h)\]
(5/5) Characterize slow downs in this dataset.
\[\phi(\tau, h) \triangleq \square_{[\tau, 20]}(\text{car_speed} \leq h)\]
\[ \begin{split}\psi_1 \triangleq \phi(0.25, 0.55) &\wedge \neg \phi(0.38, 0.55) \\&\wedge \neg \phi(0.25, 0.76)\end{split} \]
\[ \begin{split}\psi_2 \triangleq \phi(0.35, 0.17) &\wedge \neg \phi(0.35, 0.31) \\&\wedge \neg \phi(0.62, 0.17)\end{split} \]
\[\text{slow_down} \triangleq \psi_1 \wedge \psi_2\]
Infinity Norm: Let the distance between two parameters be the difference in their largest component, e.g,
\[ \text{height} \mapsto h, \text{weight} \mapsto w \] \[ d_\infty((h_1, w_1), (h_2, w_2)) \triangleq \max(|h_1 - h_2|, |w_1 - w_2|)\]
Hausdorff Distance: Let $A$ and $B$ be two sets of parameters:
\[ d^H_\infty(A, B) \triangleq \max(\sup_{a \in A} \inf_{b \in B} d_\infty(a, b), \sup_{b \in B} \inf_{a \in A} d_\infty(a, b))\]
Interpretation: The curves "\(\epsilon\)-bisimulate" each other.