arXiv:1603.00814v1 [cs.SY] 2 Mar 2016

Active Requirement Mining of Bounded-Time
Temporal Properties of Cyber-Physical Systems
Gang Chen

Zachary Sabato

Zhaodan Kong

January 15, 2018
Abstract
This paper uses active learning to solve the problem of mining bounded-time
signal temporal requirements of cyber-physical systems or simply the requirement
mining problem. By utilizing robustness degree, we formulates the requirement
mining problem into two optimization problems, a parameter synthesis problem
and a falsification problem. We then propose a new active learning algorithm
called Gaussian Process Adaptive Confidence Bound (GP-ACB) to help solving
the falsification problem. We show theoretically that the GP-ACB algorithm has a
lower regret bound thus a larger convergence rate than some existing active learning algorithms, such as GP-UCB. We finally illustrate and apply our requirement
mining algorithm on two case studies, the Ackley’s function and a real world automatic transmission model. The case studies show that our mining algorithm with
GP-ACB outperforms others, such as those based on Nelder-Mead, by an average
of 30% to 40%. Our results demonstrate that there is a principled and efficient way
of extracting requirements for complex cyber-physical systems.

1

Introduction

In this paper, we propose the use of active learning for mining bounded-time signal
temporal logic (STL) requirements of cyber-physical systems (CPSs). CPSs are characterized by the tight interaction of a collection of digital computing devices (the Cyber part) and a continuous-time dynamical system (the Physical part) [3, 22]. They
are used for modeling in many safety-critical domains, such as automotive, medical,
and aerospace industries, where the correctness of the end product is of significant
importance [16, 17, 24]. However, in many industrial settings, the requirements intended to enforce the correctness guarantee are vague and in many cases expressed
in natural languages, such as “smooth steering” and “good fuel efficiency.” This prevents the application of formal verification tools, such as Statistical Model Checking
(SMC) [31]. Further, due to the complex nature of many CPSs, writing down the appropriate requirements to reflect the desirable system properties can be challenging even
for experienced designers.
Given a system S, e.g., a Stateflow/Simulink model of a steering system, and a
requirement template ϕ with a set of unknown parameters θ , the goal of this paper is
1

to develop an improved method which can automatically infer a requirement ϕθ (often
called a specification in formal methods literature) written in signal temporal logic,
i.e., the system S satisfies the requirement ϕθ . Such a problem can be called either
a requirement mining problem or a temporal logic inference problem. In the past few
years with the introduction of the concept of robustness degree [11,13], the problem has
received increased attention and has achieved significant progress. Robustness degree
quantifies how strongly a given sample trajectory s of a system S exhibits a temporal
logic property ϕθ as a real number rather than just providing a yes or no answer. A
robustness degree of r(s, ϕθ ) means that the trajectory s can tolerate perturbations up
to the size of |r(s, ϕθ )| and still maintain its current Boolean truth value with respect to
ϕθ .
With the help of robustness degree, the requirement mining problem of a CPS
can be converted to an optimization problem for the expected robustness. Various
techniques, such as particle swarm optimization [15], simulated annealing [21], and
stochastic gradient descent algorithm [20] can then be used to solve the optimization
problem1 . Based on the nature of the search space, the requirement mining problems
can be classified into two categories, parameter estimation problems and structural inference problems. In the former case, the structure of the requirement is given but with
some unknown parameter values, for example, in a vehicular application, a requirement structure may be known as F[0,τ] (v > π), which means that “eventually between
time 0 and some unspecified time τ, the speed v is greater than some unspecified value
π.” The goal of the parameter estimation problem is to identify appropriate values
for the parameters [8, 18]. In the latter example, even the structure of the requirement is unspecified. The structural inference problem is inherently hard. Candidate
formulas have to be restricted to a certain template with which a partial order is well
defined [19–21]. This paper focuses on the parameter estimation problem, but there are
significant implications for structural inference as well.
Due to the hybrid nature of CPSs, the robustness degree function can be highly
nonlinear. Furthermore, many CPSs are stochastic because of various uncertainties inherent to the system and its mathematical model. These complexities added together
makes uniform sampling method inappropriate to solve the optimization problem (there
are even cases in which the exact probability distribution over the parameter space is
unknown a priori). Monte-Carlo techniques have been shown to be an effective sampling method to tackle the issue [2, 18]. It is worth pointing out that these techniques
may suffer from slow convergence, meaning that the inference procedure may take a
long time. In many applications, a quick verdict is needed, consider for instance an
online diagnosis of a faulty safety-critical system.
In this paper, we use active learning to partly mitigate the need for a large number of iterations during optimization. The idea behind active learning is to accelerate
convergence by actively selecting potentially “informative” samples, in contrast with
random sampling from a predefined distribution [25, 28]. Active learning can be explained with a supervised video classification problem. With passive learning, a large
amount of labeled data is needed for classification, e.g., cat videos vs. non cat videos.
1 Other optimization algorithms that have been used to solve similar optimization problems related to
verification/falsification include rapidly exploring random tree (RRT) [12], cross-entropy method [27], Tabu
search [1], and Ant Colony Optimization (ACO) [4].

2

Labeling itself involves an oracle, e.g., a human, and it might be time consuming. Further, much of the data may be redundant, not contributing much to the classification.
With active learning, based on the current information gathered about the data distribution, the learning algorithm only asks for the label of the most informative data. In
our setting, the CPS model together with a stochastic model checker will serve as an
oracle, providing the learner an approximate expected robustness degree based on the
current most informative parameter.
Contributions The main contribution of this paper is an active learning based scheme
for requirement mining of cyber-physical systems. It unifies two complementary camps
of requirement mining and verification philosophies: one is model based [2,4,6,18,27],
and the other is data driven [8, 19, 21]. In our method, models are used as oracles, generating data which enables our method to gain knowledge of the system. This helps
focusing ongoing searches in promising parameter ranges, and thus eliminating unnecessary samples. The philosophy of our paper is similar to simulation based optimization [14] but with a particular focus on utilizing machine learning techniques. Second,
instead of using existing learning algorithms, we develop a new active learning algorithm called Gaussian Process Adaptive Confidence Bound (GP-ACB). We prove
that our GP-ACB algorithm converges faster than Gaussian Process Upper Confidence
Bound (GP-UCP) algorithm [30], a state-of-the-art active learning algorithm. Third, we
integrate our GP-ACB algorithm with an existing verification tool, called Breach [10].
Using an automatic transmission controller as an example system, we show that the
efficiency of Breach can be improved by as much as 40%.
Organization This paper is subdivided into the following sections. Section 2 discusses the relevant background on signal temporal logic and Gaussian processes. Section 3 formally defines the requirement mining problem and shows how to transform
the problem into an optimization problem with the help of robustness degree. Section 4
discusses our GP-ACB algorithm. Section 5 provides two case studies to demonstrate
our algorithm, an academic example with Ackley’s function as the target function and
an automotive example. Section 6 concludes the paper.

2
2.1

Preliminaries
Signal Temporal Logic

Given two sets A and B, F (A, B) denotes the set of all functions from A to B. Given
a time domain R+ := [0, ∞), a continuous-time, continuous-valued signal is a function
s ∈ F (R+ , Rn ). We use s(t) to denote the value of signal s at time t, and s[t] to denote
the suffix of signal s from time t, i.e., s[t] = {s(τ)|τ ≥ t}.
Signal temporal logic (STL) [23] is a temporal logic defined over signals. STL is a
predicate logic with interval-based temporal semantics. The syntax of STL is defined
as
ϕ := f (s) ∼ d|¬ϕ|ϕ1 ∧ ϕ2 |ϕ1 ∨ ϕ2 |F[a,b) ϕ|G[a,b) ϕ,
(1)

3

where a and b are non-negative finite real numbers, and f (s) ∼ d is a predicate where
s is a signal, f ∈ F (Rn , R) is a function, ∼∈ {<, ≥}, and d ∈ R is a constant. The
Boolean operators ¬ and ∧ are negation (“not”) and conjunction (“and”), respectively.
The other Boolean operators are defined as usual. The temporal operators F and G
stand for “Finally (eventually)” and “Globally (always)”, respectively.
The semantics of STL is recursively defined as
s[t] |= ( f (s) ∼ d)
s[t] |= ϕ1 ∧ ϕ2
s[t] |= ϕ1 ∨ ϕ2
s[t] |= G[a,b) ϕ
s[t] |= F[a,b) ϕ

iff
iff
iff
iff
iff

f (s(t)) ∼ d
s[t] |= ϕ1 and s[t] |= ϕ2
s[t] |= ϕ1 or s[t] |= ϕ2
∀t 0 ∈ [t + a,t + b), s[t 0 ] |= ϕ
∃t 0 ∈ [t + a,t + b), s.t. s[t 0 ] |= ϕ.

In plain English, F[a,b) ϕ means “within a and b time units in the future, ϕ is true”, and
G[a,b) ϕ means “for all times between a and b time units in the future ϕ is true”.
STL is equipped with a robustness degree [11, 13] (also called “degree of satisfaction”) that quantifies how well a given signal s satisfies a given formula ϕ. The
robustness is calculated recursively as follows
r(s, ( f (s) < d),t)
r(s, ( f (s) ≥ d),t)
r(s, ϕ1 ∧ ϕ2 ,t)
r(s, ϕ1 ∨ ϕ2 ,t)
r(s, G[a,b) ϕ,t)

= d − f (s(t))
= f (s(t)) − d

= min r(s, ϕ1 ,t), r(s, ϕ2 ,t) 
= max r(s, ϕ1 ,t), r(s, ϕ2 ,t)
= min r(s, ϕ,t 0 )

r(s, F[a,b) ϕ,t) =

t 0 ∈[t+a,t+b)

max

r(s, ϕ,t 0 ).

t 0 ∈[t+a,t+b)

We use r(s, ϕ) to denote r(s, ϕ, 0). If r(s, ϕ) is large and positive, then s would have to
change by a large deviation in order to violate ϕ.
Parametric signal temporal logic (PSTL) is an extension of STL where the bound d
and the endpoints of the time intervals [a, b) are parameters instead of constants [6]. We
denote them as scale parameters π = [π1 , ..., πnπ ] and time parameters τ = [τ1 , ..., τnτ ],
respectively. A full parameterization is given as [π, τ]. The syntax and semantics of
PSTL are the same as those of STL. A valuation θ is a mapping that assigns real values
to the parameters appearing in an PSTL formula. A valuation θ of an PSTL formula ϕ
induces an STL formula ϕθ . For example, if ϕ = F[τ1 ,τ2 ) (x < π1 ) and θ ([π1 , τ1 , τ2 ]) =
[0, 0, 3], then ϕθ = F[0,3) (x < 0).

2.2

Gaussian Processes

Formally, a Gaussian process (GP) is defined as a collection of random variables, any
finite linear combination of which have a joint Gaussian distribution [26]. A simple
example of a Gaussian process is a linear regression model f (~x) = φ (~x)T ~w, where ~x ∈
Rn , φ ∈ F (Rn , RN ), which maps an n-dimensional~x to an N-dimensional feature space
(a feature is an individual, measurable property of a function space), and ~w ∼ N (~0, Σ),
a zero mean Gaussian with covariance matrix Σ. Any GP is completely specified by its

4

mean function m(~x) and its covariance function or kernel k(~x, ~x0 )
m(~x) = E[ f (~x)],
k(~x, ~x0 ) = E[( f (~x) − m(~x))( f (~x0 ) − m(~x0 ))].
As an example, for the linear regression model,
E[ f (~x)] = φ (~x)T E[~w],
E[ f (~x) f (~x0 )] = φ (~x)T E[~w~wT ]φ (~x0 ) = φ (~x)T Σφ (~x0 ).
A flat (or even zero) mean function m(~x) is chosen in the majority of cases in the
literature. Such a choice does not cause many issues since the mean of the posterior
process in not confined to zero. There is a large set of available kernels k(~x, ~x0 ). Two
common ones, which are also used in this paper, are [5]
• Gaussian kernel with length-scale l > 0, k(~x1 ,~x2 ) = exp(−|~x1 −~x2 |2 /(2l 2 )), where
|.| is the Euclidean length;
• Matérn kernel with length-scale l > 0
21−ν
k(~x1 ,~x2 ) =
Γ(ν)

!ν
√
2ν|~x1 −~x2 |
Kν
l

!
√
2ν|~x1 −~x2 |
,
l

where Kν is the modified Bessel function and ν is a positive parameter.

3

Requirement Mining Problem Formulation

In this section, we first provide some background on our cyber-physical system models.
We then formally define the requirement mining problem. Finally, we show how to
formulate the requirement mining problem as an optimization problem.

3.1

Cyber-Physical Systems

In this paper, we study autonomous (closed-loop) cyber-physical systems. Notations
from [2, 27] are adopted here. A system S maps an initial condition (or uncontrolled
environmental conditions, e.g., road conditions)~x0 ∈ X0 ⊂ Rnx to a discrete-time output
signal ~y ∈ F ([0, T ],Y ) with Y ⊂ Rny and T as the finite maximal simulation time.
We assume both X0 and Y can be represented as the Cartesian product of intervals
[a1 , b1 ] × [a2 , b2 ] × . . . [an , bn ], where ai , bi ∈ R.

3.2

Problem Statement

Formally, in this paper, we solve the following problem.
Problem 1. Given a system S with an initial condition set (or uncontrolled environmental condition set) X0 ⊂ Rnx and a parametric signal temporal logic formula ϕθ

5

with unknown parameters θ ∈ Θ ⊂ Rnθ , where Θ is the set of feasible valuation, find a
valuation θ such that
∀~x0 ∈ X0 : S(~x0 )[0] |= ϕθ .
(2)
That is to say, the output signal ~y of the system S, starting from any initial condition
~x0 ∈ X0 , satisfies ϕθ at time 0. We write S(~x0 ) |= ϕθ as shorthand for S(~x0 )[0] |= ϕθ .

3.3

Requirement Mining as Optimization

Problem 1 is subject to the curse of dimensionality. If we solve Problem 1 directly,
the dimension of the search space is nx + nθ . In this paper, we use the following three
methods to mitigate the computational complexity.
• To reduce the search space’s dimension, we follow the idea described in [18].
We divide Problem 1 into two sub-problems: a parameter synthesis problem
(Problem 2) having a dimension of nθ and a falsification problem (Problem 3)
having a dimension of nx .
• We then develop an active learning algorithm to progressively reduce the volume
of the search space. The active learning algorithm focuses only on “informative”
initial states, meaning it does not need to search the entire initial condition set
X0 .
• Finally, we take advantage of the monotonicity property of PSTL [18, 20, 21]. If
a parameter has been found that solves Problem 2, then there is no need to check
for parameters that make the requirement more restrictive, as these parameters
surely do not constitute an optimal solution.
The flowchart to solve Problem 1 is shown in Fig. 1.

Figure 1: Flowchart for solving Problem 1. Our algorithm is based on the Breach
toolbox [10, 18]. Our new active learning algorithm is used in the falsification step
(shown in blue).

6

Problem 2. Parameter Synthesis Given a system S with a set of inputs X̄0 = {~x0i ∈
X0 , i = 1, 2, · · · , ns }, where ns is the number of counter-example traces obtained from
Problem 3, and a PSTL formula ϕθ with unknown parameters θ ∈ Θ ⊂ Rnθ , find a
valuation θ to solve
max(0, ε − min (r(S(~x0 ), ϕθ ))),
(3)
~x0 ∈X̄0

θ

where ε > 0 us a user-specified bound.
Problem 3. Falsification Given a system S with an initial condition set (or uncontrolled environmental condition set) X0 ⊂ Rnx and a PSTL formula ϕθ with particular
parameters θ ∈ Θ, find an initial condition ~x0 ∈ X0 to solve
min (r(S(~x0 ), ϕθ )).

~x0 ∈X0

(4)

The max function max(0, ε − ·) in Eqn. (3) is a modified hinge loss function. As
the minimum of the robustness, min(r(S(~x0 ), ϕθ )), is positive, the loss function rewards
values that are close to the bound 0 and at the same time positive. It is utilized here to
tackle the issue related to the non-uniqueness of solutions to the requirement mining
problem, as pointed out in [18]. For a particular θ , the min functions in Eqn. (3) and
Eqn. (4) reward initial states that lead to negative robustness degrees. Their goals are
to find an initial state which leads to a trace that does not meet the requirement ϕθ . The
max-min function, Eqn. (3), then finds a parameter θ , and, in turn, a requirement ϕθ
such that for any initial state x0 ∈ X0 , the output of the system has a positive robustness
degree that is smaller than ε. This means that the system satisfies the requirement ϕθ ,
but only barely. Formally,
Lemma 1. A formula obtained by solving Problem 2 and Problem 3 together is a
solution to Problem 1. I.e., if a formula ϕθ ∗ , where
θ ∗ = argmax(0, ε − min(r(S(~x0 ), ϕθ )))
~x0

θ

and furthermore ∀~x0 ∈ X0 , r(S(~x0 ), ϕθ ∗ ) > 0, the statement (2) hold.
Proof. Assume there is a parameter θ 0 obtained by solving Problem 2 and Problem
0
0
0
3, and ~x0 ∈ X0 : S(~x0 )[0] 2 ϕθ 0 . According to Problem 3, a ~x0 ∈ X0 that meets the
requirements cannot be found. Thus, Lemma 1 has been proven.
The most time-consuming part of solving Problem 1 is the generation of a trace
given an initial state ~x0 . For the parameter synthesis problem, there is no need to generate traces. Moreover, according to [18], since PSTL satisfies the important property
of monotonicity, the solution is quite efficient, via a binary search algorithm [12], for
example. The falsification problem, on the other hand, does need a large number of
traces being generated. Therefore, finding a way to minimize the number of traces
needed in the falsification step will benefit the requirement mining process greatly.
In this paper, we solve the falsification problem with a new active learning algorithm
called Gaussian Process Adaptive Confidence Bound (GP-ACB). We will show theoretically (in Section 4) and empirically (in Section 5) the effectiveness of our algorithm
in reducing the computational time.
7

4

Active Learning Algorithm

In the section, we propose an active learning algorithm, called Gaussian Process Adaptive Confidence Bound (GP-ACB) algorithm, to solve the falsification problem mentioned in Section 3. It is inspired by Gaussian process upper confidence bound (GPUCB) [30]. We analyze the regret bound of GP-ACB and show that it can achieve the
same regret bound with a higher probability than GP-UCB.

4.1

Gaussian Process Adaptive Confidence Bound Active Learning
Algorithm

Active learning algorithms are originally developed to solve classification problems
when an oracle is needed to provide labels [28]. The process of obtaining labels from
the oracle can be expensive in terms of both time and money. Thus, the goal of any
active learning algorithm is to achieve high classification or regression accuracy by
using the fewest labeled instances. The requirement mining problem suffers from a
similar issue as elaborated at the end of Section 3. Our oracle is a simulator, e.g., a
Stateflow/Simulink model. Given the complexity of many CPS models, to obtain a
trace from the simulator can be costly in time. Thus, we need to decrease the number
of simulations needed to learn a formula.
One active learning algorithm is called Gaussian process upper confidence bound
(GP-UCB) [30]. At each step t, it solves the following problem
1

~xt = argmax mt−1 (~x) + βt 2 σt−1 (~x),

(5)

~x∈D

where D is the search space (D = X0 for the requirement mining problem), βt is a
function of t and independent of ~x (an example of βt will be given later), mt−1 (.) and
σt−1 (.) are the mean and covariance function of the Gaussian process, respectively,
and ~xt is the instance that will be inquired at step t, meaning the label of ~xt will be
obtained from the oracle. The GP-UCB algorithm balances the classical exploitationexploration trade-off by combining two strategies: the first term tends to pick those
points that are expected to achieve high rewards (exploitation); and the second terms
tend to pick those points that are uncertain (exploration).
The second term of Eqn. (5) only depends on the covariance function σ (~x), which
can potentially make the exploration somewhat random and inefficient. To address
this problem, we propose an algorithm called Gaussian Process Adaptive Confidence
Bound (GP-ACB) by adding a normalization term ηm (x) to Eqn. (5) as follows:
1

1

~xt = argmax mt−1 (~x) + ηm (~x) 2 βt 2 σt−1 (~x),
~x∈D

where ηm (~x) normalizes the mean mt−1 (~x) and can be written explicitly as
ηm (~x) =

mt−1 (~x) − min(mt−1 (~x))
.
max(mt−1 (~x)) − min(mt−1 (~x))

8

(6)

It is quite obvious that 0 ≤ ηm (~x) ≤ 1. ηm (~x) serves two main purpose here. First, it
acts as an adaptive factor to uncertainty and favors exploration directions associated
with increasing rewards. Thus, it can improve the exploration efficiency. Second, it
provides an adaptive upper quantile of the marginal posterior P( f (~x) |~yt−1 ), where~yt−1
is a vector containing all the observations until time t − 1. In this paper, we assume that
the observation at time t, yt ∈ R, is yt = f (~x) + εt with εt ∼ N (0, σ 2 ) and σ 2 known.
Pseudocode for the GP-ACB algorithm is provided in Algorithm 1.
Algorithm 1: GP-ACB Algorithm
Input:
Search space D (X0 for the requirement mining problem);
GP priors m(~x)0 = 0 and σ0 ;
Kernel function k;
Maximal simulation time T
1: for i = 1 to T do
2:
Perform Bayesian update to obtain mt−1 (~x) and σt−1 (~x);
3:
Calculate the normalization factor ηm (~x);
4:
5:

4.2

1

1

Choose ~xt = argmax~x∈D mt−1 (~x) + ηm (~x) 2 βt 2 σt−1 (~x);
Calculate ~yt = f (~xt ) + εt with εt ∼ N (0, σ 2 ).

Regret Bound of GP-ACB

The goal of any learning algorithm can be stated as follows: given an unknown reward
T
function f ∈ F (D, R), maximize the sum of rewards ∑t=1
f (~xt ), which is equivalent
∗
∗
to finding a ~x such that ~x = argmax~x∈D f (~x). A concept called regret bound can be
used to quantify the convergence rate of a learning algorithm [7, 28, 29]. First, the
instantaneous regret at time t is defined as rt = f (~x∗ ) − f (~xt ). Then, the cumulative
T
regret RT after T rounds is the sum of instantaneous regrets RT = ∑t=1
rt . A desired
property of the learning algorithm is then to guarantee limT →∞ RT /T = 0, implying
the convergence to the global maximum ~x∗ . Finally, the bounds on the average regret
RT /T are directly related to the convergence rate of the learning algorithm. The lower
the bound is, the faster the algorithm converges. This section investigates the regret
bound of the GP-ACB algorithm.
Our proofs on the regret bound follow those in [29]. Here we only consider the
cases when the search space is finite, i.e., |D| < ∞.
Lemma 2. Pick δ ∈ (0, 1) and set βt = 2 log(|D|πt /δ ), where ∑t≤1 πt−1 = 1, πt > 0.
Then,
1/2
| f (~x) − mt−1 (~x)| ≤ ηm (~x)1/2 βt σt−1 (~x), ∀~x ∈ D and ∀t ≥ 1
holds with probability ≥ 1 − δ ηm (~x) .
Proof. For ~x ∈ D and t ≥ 1. It is known that conditioned on ~yt−1 = (y1 , · · · , yt−1 ),
2 (~
{~x1 , · · · ,~xt−1 } are deterministic. Further, f (~x) v N (mt−1 (~x), σt−1
x)). Now if r v

9

N(0, 1), then
2

2 /2−c(l−c)

Pr{r > c} = e−c /2 (2π)−1/2 e−(l−c)
2
2
≤ e−c /2 Pr{r > 0} = (1/2)e−c /2 .
R

dr
1/2

for c > 0, as e−c(r−c) ≤ 1 for r ≥ c. We have Pr{| f (~x)−mt−1 (~x)| > ηm (~x)βt σt−1 (~x)} ≤
1/2
e−ηm (~x)βt /2 . Set r = ( f (~x) − mt−1 (~x))/σt−1 (~x) and c = ηm (~x)1/2 βt . After applying
the adaptive bound, we have
1/2

| f (~x) − mt−1 (~x)| ≤ ηm (~x)1/2 βt

σt−1 (~x) ∀~x ∈ D

holds with probability ≥ 1 − |D|e−ηm (~x)βt /2 . Choosing |D|e−ηm (~x)βt /2 = δ /πt , e.g., with
πt = π 2t 2 /6, and using the adaptive bound for t ∈ N, the statement holds.
1/2

Lemma 3. Fix t ≥ 1, if | f (~x) − mt−1 (~x)| ≤ ηm (~x)1/2 βt
1/2
regret rt is bounded by 2βt σt−1 (~xt ).

σt−1 (~x), ∀~x ∈ D, then the
1/2

Proof. According to the definition of ~x∗ , mt−1 (~xt ) + ηm (~xt )1/2 βt σt−1 (~xt )
1/2
≥ mt−1 (~x∗ ) + ηm (~x∗ )1/2 βt σt−1 (~x∗ ) ≥ f (~x∗ ). Therefore, the instantaneous regret
rt = f (~x∗ ) − f (~xt )
1/2
≤ ηm (~xt )1/2 βt σt−1 (~xt ) + mt−1 (~xt ) − f (~xt )
1/2
1/2
≤ 2ηm (~xt )1/2 βt σt−1 (~xt ) ≤ 2βt σt−1 (~xt )
Lemma 4. Pick δ ∈ (0, 1) and set βt = 2 log(πt /δ ), where ∑t≥1 πt−1 = 1, πt > 0. Then,
1/2

| f (~x) − mt−1 (~x)| ≤ ηm (~x)1/2 βt

σt−1 (~x) ∀t ≥ 1

holds with probability ≤ 1 − δ ηm (~xt ) .
Proof. For ~x ∈ D and t ≥ 1. Conditioned on yt−1 = {y1 , · · · , yt−1 }, {~x1 , · · · ,~xt−1 }
2 (~
are deterministic. Further, f (~xt ) ∼ N (mt−1 (~x), σt−1
x)). According to Lemma 2,
1/2

Pr{| f (~xt ) − mt−1 (~xt )| > ηm (~xt )1/2 βt σt−1 (~xt )} ≤ e−ηm (~xt )βt /2 . Since e−βt /2 = δ /πt ,
and with the adaptive bound for t ∈ N, the statement holds.
Lemma 5. Set Lt = max(mt (~x)) − min(mt (~x)), ∀~x ∈ D, and let βt be defined as in
Lemma 4, then
1/2
1 − ηm (~xt )1/2 ≤ βt σt−1 (~xt )/Lt ∀t ≥ 1
1/2

Proof. Set mt−1 (~xm ) = max(mt−1 (~x)), ∀~x ∈ D, according to GP-ACB, ηm (~xt )1/2 βt
1/2
mt−1 (~xt ) ≥ ηm (~xm )1/2 βt σt−1 (~xm ) + mt−1 (~xm ), then
1/2

mt−1 (~xm ) − mt−1 (~xt−1 ) ≤ ηm (~xt )1/2 βt
⇒ 1 − ηm (~xt )1/2 ≤
≤

1/2
βt
Lt

1/2
βt
Lt

1/2

σt−1 (~xt ) − ηm (~xm )1/2 βt

(ηm (~xt )1/2 σt−1 (~xt ) − ηm (~xm )1/2 σt−1 (~xm ))
1/2

(ηm (~xt )1/2 σt−1 (~xt ) ≤ βt

10

σt−1 (~xt )/Lt

σt−1 (~xm )

σt−1 (~xt )+

Remark 1. Lemma 5 shows that when the scale of the function Lt is large, ηm (~x)
will be close to 1, meaning the GP-ACB algorithm degrades to GP-UCB. Conversely,
when the scale of function is large, mt (~x) will play a more important role in the search
process, driving the algorithm to be very greedy. To investigate the effects of the scaling
function on the optimization performance, a numerical experiment has been conducted
and the results are shown in Section 5.1.
Define γT as the maximum information gain after T rounds as follows [29]:
0

γT = max
T 0 ≤T

1 T
2
(~xt ))
∑ log(1 + σ −2 σt−1
2 t=1

According to [29], if the search space D ∈ Rd is compact and convex, where d is the
dimension of the search space, with the assumption that the kernel function satisfies
0
k(~x,~x ) 6 1, we have
• γT = O((log T )d+1 ) for Gaussian kernel;


• γT = O T d(d+1)/(2ν+d(d+1)) (log T ) for Matérn kernels with ν > 1.
We can finally obtain the following bound for the GP-ACB algorithm.
Theorem 1. Let δ ∈ (0, 1), βt = 2 log(|D|t 2 π 2 /6δ ) , m = mint=(1,··· ,T ) (ηm (~xt )) and
n = maxt=(1,··· ,T ) (ηm (~xt )). Running GP-ACB results in a regret bound as follows
p
Pr{RT ≤ nC1 T βT γT , ∀T ≥ 1} ≥ 1 − δ m ,
(7)
where C1 = 8/ log(1 + σ −2 ).
Proof. Define the information gain I as follows:
I(yT , fT ) =

1 T
2
(~xt )),
∑ log(1 + σ −2 σt−1
2 t=1

where f T = ( f (~x1 ), . . . , f (~xT ))0 ∈ RT . According to Lemma 2 and Lemma 4, the regret
2 (~
bound {rt2 ≤ 4ηm (~xt )βt σt−1
xt ), ∀t ≥ 1} holds with probability ≥ 1 − δ ηm (~xt ) ≥ 1 − δ m .
As βt is non-decreasing, we have
2
2
2
(~xt ))
4ηm (~x)βt σt−1
(~xt ) ≤ 4nβT σ 2 (σ −2 σt−1
(~xt ) ≤ 4nβT σ 2 S log(1 + σ −2 σt−1

(8)

2 (~
where S = σ −2 / log(1 + σ −2 ), since σ −2 σt−1
xt ) ≤ σ −2 k(~xt ,~xt ) ≤ σ −2 ,
−2
2
2
C1 = 8/ log(1 + σ ) ≥ 8σ and h ≤ S log(1 + h2 ) f or h ∈ [0, σ −2 ]. As C1 = 8σ 2 S,
for T ≥ 1 we have
T
T
T 1
2 (~
−2 2
xt ))
rt2 ≤ ∑t=1
4ηm (~x)βt σt−1
xt ) ≤ n ∑t=1
∑t=1
2 βT C1 log(1 + σ σt−1 (~
≤ nC1 βT γT .
T
According to Cauchy-Schwarz inequality, R2T ≤ T ∑t=1
rt2 . Theorem 1 has been proven.

11

Remark 2. The regret bound of the GP-UCB algorithm is [29]
p
Pr{RT ≤ C1 T βT γT , ∀T ≥ 1} ≥ 1 − δ .
With the same parameter setting, the regret bound of our GP-ACB algorithm is shown
as Eqn. (7). Based on the bound of η(~x) shown in Lemma 5 and the definition of
the information gain γT , we know that σt−1 (~xt ) is close to 0 when T is large, which
means m and n in Theorem 1 are close to one when iteration T is large and are close
to zero when iteration T is small. This indicates that GP-ACB algorithm is greedy at
the beginning and degrades to GP-UCB algorithm when iteration T is large. Since
0 < m, n 6 1, we can get the conclusion that the GP-ACB algorithm can get the same
regret bound more efficient than that of the GP-UCB algorithm. The regret bound can
be easily translated into convergence rate. The maximum maxt≤T f (~xt ) in the first T
iterations is no further from f (~x∗ ), where ~x∗ is the global optimum, than the average
regret RT /T . Thus, compared with GP-UCB, on average, the GP-ACB algorithm has
a higher or equal convergence rate.

5

Case Studies

To demonstrate the capability of GP-ACB, in this section, we first use it to solve a
global optimization problem with Ackley’s function as the target function. The performance of GP-ACP is compared with those of other active learning algorithms. We
then use GP-ACB to solve a full scale requirement mining problem of an automatic
transmission system, a benchmark used widely in CPS community [17, 18, 27]. In both
cases, GP-ACB outperforms other active learning algorithms as well as some other
state-of-art optimization algorithms such as Nelder-Mead.

5.1

Global Optimization of Ackley’s Function

To verify the performance of the proposed GP-ACB algorithm, we compare the GPACB algorithm with four types of Gaussian-Process-based strategy: (i) GP-UCB active
learning, (ii) Batch-greedy UCB active learning [9], (iii) pure exploration, i.e., choosing points of maximum variance at each step, and (iv) pure exploitation or greedy, i.e.,
choosing points of maximum mean at each step. We use Ackley’s function (shown in
Fig. 2.(a)) as the target function. Its formula is as follows,
√
2
2
f (x, y) = −20e−0.2 0.5(x +y ) − e0.5(cos(2πx)+cos(2πy)) + e + 20,
where e is the observation noise with zero mean and variance σ 2 at 0.025. The search
space D = [−5, 5]2 is randomly discretized into 1000 points. We run each algorithm
for T = 58 iterations with sampling time δ = 0.1. Since the global minimum of the
Ackley’s function (x∗ , y∗ ) is known (unknown to the learning algorithms though), for
the i-th trial, if (xti , yti ) is the solution obtained by running the algorithm for t iterations,
t
then mean regret for the algorithm at time t is R̄t = ∑Ni=0
[ f (xti , yti )− f (x∗ , y∗ )]/Nt , where
Nt is the number of trials. In this case study, we set Nt = 1000. Each trial is initialized
randomly.
12

(a)
6

6
GP-ACB
GP-UCB
Batch greedy UCB
Pure exploration
Pure exploitation

4

GP-ACB
GP-UCB
Batch greedy UCB
Pure exploration
Pure exploitation

5

Mean Regret

Mean Regret

5

3
2
1

4
3
2
1

0

0
0

10

20

30

40

50

0

10

Iterations

20

30

40

50

Iterations

(b)

(c)

Figure 2: (a) Ackley’s function. (b) and (c) compares the performance of GP-ACB with
i i
those of other strategies. The mean regret over 1000 trails R̄(t) := R̄t = ∑1000
i=0 [ f (xt , yt )−
∗
∗
f (x , y )]/1000 is chosen as the performance metric. (b) shows the comparison results
with Gaussian kernel. (c) shows the comparison results with Matérn kernel.
Fig. 2(b) and Fig. 2(c) show the comparison of the mean regret R̄t incurred by the
different Gaussian Process based algorithms with Gaussian kernel and Matérn kernel,
respectively. With both kernels, GP-ACB outperforms the others. For instance, GPUCB arrives at its minimum regret in an average of 58 iterations; while GP-ACB arrives
at its minimum regret in an average of 45 iterations. Another interesting observation is
that pure exploitation (greedy) strategy on average converges quicker than others. But
the regret it converges to is on average higher than others, implying the convergence to
local minimums. As for kernels, for this particular case, Matérn kernel outperforms the
Gaussian kernel. This is not supervising, given that the Ackley’s function (as shown
in Fig. 2(a)) is quite “non-smooth” and Matérn kernel is designed to capture nonsmoothness.
Remark 1 shows that the range of the mean function m(~x) at time t,
Lt = max(mt (~x)) − min(mt (~x)),
affects the performance of the GP-ACB algorithm. When the range Lt is large, the
13

6

Mean Regret After T Iterations

6

Mean Regret

5
4
3
2
1
0

GP-ACB
GP-UCB
Batch greedy UCB
Pure exploration
Pure exploitation

5
4
3
2
1
0

0

10

20

30

40

50

0

Iterations

5

10

15

Iterations

(a)

(b)

Figure 3: (a) The performance of the GP-ACB’s algorithm with respect to the
i i
scaling factor ξ . The mean regret over 1000 trails R̄(t) := R̄t = ∑1000
i=0 [ f (xt , yt ) −
∗
∗
f (x , y )]/1000 is chosen as the performance metric. (b) The effects of the scaling factor ξ on different algorithms. The mean regret at time T over 1000 trails
i
i
∗ ∗
∑1000
i=0 [ f (xT , yT ) − f (x , y )]/1000 is chosen as the performance metric. Here T = 58.
GP-ACB algorithm degrades to the GP-UCB algorithm. In this paper, we use a scale
factor ξ to change the range of the reward or cost function. Instead of optimizing
f (~x) directly, we scale it by ξ first and then solve the optimization problem with a
new reward or cost function ξ f (~x). To demonstrate the effects, Fig. 3(a) shows the
performance of GP-ACB with different scaling factors. It shows that when the scaling
factor ξ is large, the algorithm prefers exploitation over exploration and has the danger of trapping in a local optimum; when the scaling factor ξ is small, the algorithm
prefers exploration over exploitation and it may take more than necessary time to explore irrelevant regions. Thus, a proper ξ needs to be selected to balance the trade-off
between exploration and exploitation. Fig. 3(b) shows the effects of the scaling factor
ξ on different algorithms. It shows that when the scaling factor ξ is large, the GP-UCB
and GP-ACB algorithms have the same mean regret after 58 iterations, implying GPACB has degraded to GP-UCB. The pure exploration and pure exploitation algorithms’
performance are not effected by the scaling factor ξ .

5.2

Requirement Mining on an Automatic Transmission Model

The model used in the following study is the same as the one used in [18], a closed-loop
model of a four-speed automatic transmission, shown in Fig 4. The model contains all
necessary mechanical components, including engine, transmission and the longitudinal
chassis dynamics. In the model, the throttle position and brake torque are the input
signals. With the current gear selection, the transmission ratio (Ti) can be computed
through the transmission block, and the output torque can be obtained with the engine
speed (Ne), gear status and transmission RPM.
We tested three different template requirements which are the same with [18], thus
a comparison study can be conducted. The three template requirements are as follows:

14

Figure 4: Closed-loop Simulink model of an automatic transmission and controller,
whose exogenous inputs are the throttle position and brake torque.
1. Requirement ϕsp rpm (π1 , π2 ), which has a strong correlation with safety requirements characterizing the operating region for the engine parameters speed and
RPM, specifying that always the speed is below π1 and RPM is below π2 .
G((speed < π1 ) ∧ (RPM < π2 )).
2. Requirement ϕrpm100 (π, τ), which measures the performance of the closed loop
system. The value for τ specifies how fast the vehicle can reach a certain speed,
and the value for π can specify the lowest RPM needed to reach the above speed.
The formula specifies that the vehicle cannot reach the speed of 100 mph in τ
seconds with RPM always below π:
¬(F[0,τ] (speed > 100) ∧ G(RPM < π)).
3. Requirement ϕstay (τ), which encodes undesirable transient shifting of gears,
specifying that whenever the system shifts to gear 2, it dwells in gear 2 for at
least τ seconds:


G gear 6= 2 ∧ F[0,ε] gear = 2 ⇒ G[0,τ] gear = 2 .
Our requirement mining algorithm as shown in Fig. 1 and elaborated in Section
3.3 is implemented to mind requirements for the automatic transmission model. Our
algorithm is based on the Breach toolbox [10] with the falsification problem solved
by GP-ACB. The Breach toolbox uses the Nelder-Mead algorithm for falsification [10,
18]. Section 5.1 shows that the scaling factor affects the performance of the GP-ACB
algorithm. We first run a few test trials in order to find the optimal scaling factor, the
results of which are shown in Table 1. It can be seen that when scaling factor is set
to 0.5, the time spent on falsification, the time spent on parameter synthesis and the
number of simulations are all at their lowest values. Thus, the scaling factors are set to
0.5 for all the following experiments.
15

Table 1: Requirement mining results for GP-ACB with different scaling factors. In this
table and Table 2, “Parameter Values” are the mined parameter values. For instance,
parameter values (4849, 155) together with the formula template ϕsp rpm (π1 , π2 ) means
that the mined formula is G((speed < 4849) ∧ (RPM < 155)). “Fals.(s)” is the CPU
time spent on solving the falsification problem. “Synth.(s)” is the CPU time spent
on solving the parameter synthesis problem. “#Sim.” is the number of simulations.“Robustness” is the robustness degree corresponding to the mined parameters.
Scaling Factor
Requirement Mining Results
ϕsp rpm (π1 , π2 ) Parameter Values Fals.(s) Synth.(s) #Sim. Robustness
0.1
(4849, 155)
112
16.1
393
0.1541
0.25
(4846, 155)
109
17.4
385
0.3510
(4849, 155)
67
15.4
255
0.7108
0.5
0.75
(4846, 155)
79
15.6
276
0.8197
1
(4847, 155)
107
16.6
367
1.5098

The comparison results, averaged over 20 randomly started trails, for GP-ACB with
Gaussian kernel, GP-ACB with Matérn kernel, GP-UCB and Nelder-Mead are shwon
in Table 2. The results show GP-ACB with Matérn kernel outperforms the others in
terms of the times spent on falsification, the times spent on parameter synthesis and the
numbers of simulations. For instance, in mining the formula ϕsp rpm (π1 , π2 ), GP-UCB
saves on average 10% of simulation number compared with Nelder-Mead, while GPACB with Matérn kernel saves up to about 40%. The same level of improvement is
observed for the other two requirements, ϕrpm100 (π, τ) with a 40% improvement and
ϕstay (π) with a 30% improvement.
Table 2: Requirement mining results for GP-ACB with Gaussian kernel, GP-ACB with
Matérn kernel, GP-UCB with Matérn kernel, and Nelder-Mead algorithm.
Template
Requirement Mining Results
ϕsp rpm (π1 , π2 )
Parameter Values Fals.(s) Synth.(s) #Sim. Robustness
GP-ACB(Gaussian)
(4845, 155)
100
15.6
330
1.2812
GP-ACB(Matérn)
(4849, 155)
67
15.4
255
0.7108
(4844, 155)
97
15.4
334
0.7425
GP-UCB(Matérn)
Nelder-Mead
(4857, 155)
112
13.3
380
0.6738
ϕrpm100 (π, τ)
Parameter Values Fals.(s) Synth.(s) #Sim. Robustness
GP-ACB(Gaussian)
(5997, 12.20)
64
2.0
207
0.1556
GP-ACB(Matérn)
(5997, 12.20)
59
1.9
179
0.0802
GP-UCB(Matérn)
(5997, 12.20)
63
2.0
190
0.1116
Nelder-Mead
(5997, 12.20)
104
1.4
340
0.06453
ϕstay (τ)
Parameter Values Fals.(s) Synth.(s) #Sim. Robustness
GP-ACB(Gaussian)
0.0586
296
10.6
941
0.05
GP-ACB(Matérn)
0.0586
294
10.8
940
0.05
GP-UCB(Matérn)
0.0586
363
10.6
1056
0.05
Nelder-Mead
0.0586
422
9.3
1246
0.1

16

6

Conclusions and Future Work

In this paper, we introduced an active learning method, called Gaussian Process adaptive confidence bound (GP-ACB), for mining requirements of bounded-time temporal
properties of cyber-physical systems. The theoretical analysis of the proposed algorithm showed that it had a lower regret bound thus a higher convergence rate than
other Gaussian-Process-based active learning algorithms, such as GP-UCB. By using
two case studies, one of which was an automatic transmission model, we showed that
our requirement mining algorithm outperformed other existing algorithms, e.g., those
based on GP-UCB or Nelder-Mead, by an average of 30% to 40%. Our results have
significant implications for not only the requirement mining but also the validation
and verification of cyber-physical systems. We are currently exploring the possibility
of utilizing active learning to solve the structural inference problem, i.e., to mind a
requirement without any given template.

References
[1] H. Abbas and G. Fainekos. Linear hybrid system falsification through local
search. In Automated Technology for Verification and Analysis, pages 503–510.
Springer, 2011.
[2] H. Abbas, G. Fainekos, S. Sankaranarayanan, F. Ivančić, and A. Gupta. Probabilistic temporal logic falsification of cyber-physical systems. ACM Transactions
on Embedded Computing Systems (TECS), 12(2s):95, 2013.
[3] R. Alur. Principles of cyber-physical systems. MIT Press, 2015.
[4] Y. Annpureddy, C. Liu, G. Fainekos, and S. Sankaranarayanan. S-taliro: A tool
for temporal logic falsification for hybrid systems. Springer, 2011.
[5] H. K. Anwar S and S. W. Fixed point optimization of deep convolutional neural
networks for object recognitio. pages 1131–1135. IEEE, 2015.
[6] E. Asarin, A. Donzé, O. Maler, and D. Nickovic. Parametric identification of
temporal properties. In Runtime Verification, pages 147–160. Springer, 2012.
[7] P. Auer, T. Jaksch, and R. Ortner. Near-optimal regret bounds for reinforcement
learning. In Advances in neural information processing systems, pages 89–96,
2009.
[8] E. Bartocci, L. Bortolussi, and G. Sanguinetti. Data-driven statistical learning of
temporal logic properties. In Formal Modeling and Analysis of Timed Systems,
pages 23–37. Springer, 2014.
[9] K. A. Desautels T and B. J. W. Parallelizing exploration-exploitation tradeoffs
in gaussian process bandit optimization. The Journal of Machine Learning Research, pages 3873–3923, 2014.

17

[10] A. Donzé. Breach, a toolbox for verification and parameter synthesis of hybrid
systems. pages 167–170. Springer Berlin Heidelberg, 2010.
[11] A. Donzé and O. Maler. Robust satisfaction of temporal logic over real-valued
signals. Formal Modeling and Analysis of Timed Systems, pages 92–106, 2010.
[12] T. Dreossi, T. Dang, A. Donzé, J. Kapinski, X. Jin, and J. V. Deshmukh. Efficient
guiding strategies for testing of temporal properties of hybrid systems. In NASA
Formal Methods, pages 127–142. Springer, 2015.
[13] G. E. Fainekos and G. J. Pappas. Robustness of temporal logic specifications
for continuous-time signals. Theoretical Computer Science, 410(42):4262–4291,
2009.
[14] Gosavi and Abhijit. Simulation-based optimization: An overview. pages 29–35.
Springer US, 2015.
[15] I. Haghighi, A. Jones, Z. Kong, E. Bartocci, R. Gros, and C. Belta. Spatel: a
novel spatial-temporal logic and its applications to networked systems. In Proceedings of the 18th International Conference on Hybrid Systems: Computation
and Control, pages 189–198. ACM, 2015.
[16] Z. Jiang, M. Pajic, and R. Mangharam. Cyber-physical modeling of implantable
cardiac medical devices. Proceedings of the IEEE, 100(1):122–137, 2012.
[17] X. Jin, J. V. Deshmukh, J. Kapinski, K. Ueda, and K. Butts. Powertrain control
verification benchmark. In Proceedings of the 17th international conference on
Hybrid systems: computation and control, pages 253–262. ACM, 2014.
[18] X. Jin, A. Donzé, J. V. Deshmukh, and S. A. Seshia. Mining requirements from
closed-loop control models. In Proceedings of the 16th international conference
on Hybrid systems: computation and control, pages 43–52. ACM, 2013.
[19] A. Jones, Z. Kong, and C. Belta. Anomaly detection in cyber-physical systems:
A formal methods approach. In Decision and Control (CDC), 2014 IEEE 53rd
Annual Conference on, pages 848–853. IEEE, 2014.
[20] Z. Kong, A. Jones, and C. Belta. Temporal logics for learning and detection of
anomalous behavior. IEEE Transactions on Automatic Control, accepted.
[21] Z. Kong, A. Jones, A. Medina Ayala, E. Aydin Gol, and C. Belta. Temporal
logic inference for classification and prediction from data. In Proceedings of the
17th international conference on Hybrid systems: computation and control, pages
273–282. ACM, 2014.
[22] E. A. Lee and S. A. Seshia. Introduction to embedded systems: A cyber-physical
systems approach. Lee & Seshia, 2011.
[23] O. Maler and D. Nickovic. Monitoring temporal properties of continuous signals.
Formal Techniques, Modelling and Analysis of Timed and Fault-Tolerant Systems,
pages 71–76, 2004.
18

[24] R. R. Rajkumar, I. Lee, L. Sha, and J. Stankovic. Cyber-physical systems: the next
computing revolution. In Proceedings of the 47th Design Automation Conference,
pages 731–736. ACM, 2010.
[25] A. Ramdas and A. Singh. Algorithmic connections between active learning and
stochastic convex optimization. In Algorithmic Learning Theory, pages 339–353.
Springer, 2013.
[26] Rasmussen and C. Edward. Gaussian processes for machine learning. The MIT
Press, 2006.
[27] S. Sankaranarayanan and G. Fainekos. Falsification of temporal properties of
hybrid systems using the cross-entropy method. In Proceedings of the 15th ACM
international conference on Hybrid Systems: Computation and Control, pages
125–134. ACM, 2012.
[28] B. Settles. Active learning literature survey. University of Wisconsin, Madison,
52(11):55–56, 2010.
[29] N. Srinivas, A. Krause, and S. Kakade. Gaussian process optimization in the
bandit setting: No regret and experimental design. arXiv preprint arXiv, pages
0912–3995, 2009.
[30] N. Srinivas, A. Krause, S. M. Kakade, and M. W. Seeger. Information-theoretic
regret bounds for gaussian process optimization in the bandit setting. Information
Theory, IEEE Transactions on, 58(5):3250–3265, 2012.
[31] P. Zuliani, A. Platzer, and E. M. Clarke. Bayesian statistical model checking with
application to simulink/stateflow verification. In Proceedings of the 13th ACM international conference on Hybrid systems: computation and control, pages 243–
252. ACM, 2010.

19

