Neural State Classification (NSC) is a recently proposed method for runtime predictive monitoring of Hybrid Automata (HA) using deep neural networks (DNNs). NSC predictors have very high accuracy, yet are prone to prediction errors that can negatively impact reliability. To overcome this limitation, we present Neural Predictive Monitoring (NPM), a technique that complements NSC predictions with estimates of the predictive uncertainty. These measures yield principled criteria for the rejection of predictions likely to be incorrect, without knowing the true reachability values. We also present an active learning method that significantly reduces the NSC predictor's error rate and the percentage of rejected predictions. NPM is based on the use of Bayesian techniques, Bayesian Neural Networks and Gaussian Processes, to learn respectively the predictor and the rejection rule. Our approach is highly efficient, with computation times on the order of milliseconds, and effective, managing in our experimental evaluation to successfully reject almost all incorrect predictions.
where 1 is the indicator function. A state x ∈ X is called positive w.r.t. a predictor F : X → {0, 1} if F (x) = 1. Otherwise, x is called negative (w.r.t. F ).
Finding F ∗, i.e., finding a function approximation with minimal error probability, is indeed a classical
machine learning problem, a supervised classification problem in particular, with F ∗ being the classifier,
i.e., the function mapping HA state inputs x into one of two classes: positive or negative.
Training set. In supervised learning, one minimizes a measure of the empirical prediction error w.r.t. a
training set. In our case, the training set Zt is obtained from a finite sample Xt of X by labelling the training
inputs x ∈ Xt using some reachability oracle, that is, a hybrid automata reachability checker like [
Let f be the discriminant function associated to the classifier F , i.e., the function that maps the inputs into class likelihoods. A central objective of this work is to derive, given a predictor f , a rejection criterion Rf able to identify states x that are wrongly classified by F , i.e., FNs and FPs, without knowing the true reachability value of x. Further, Rf should be optimal, that is, it should ensure minimal probability of rejection errors w.r.t. the state distribution X .
Our solution relies on enriching each prediction with a measure of predictive uncertainty: given f , we define a function uf : X → U mapping an HA state x ∈ X into some measure uf (x) of the uncertainty of f about x. The only requirements are that uf must be point-specific and should not use any knowledge about the true reachability value. The function uf is then used to build an optimal error detection criterion, as explained below.
Problem 2 (Uncertainty-based error detection). Given a reachability predictor f , a distribution X over HA states X, a predictive uncertainty measure uf : X → U over some uncertainty domain U , and a kind of error e ∈ {pe, fn, fp}, find an optimal error detection rule Gf∗,e : U → {0, 1}, i.e., a function that minimizes the probability that Gf∗,e makes a mistake in recognizing errors of type e:
Prx∼X (e(x) 6= Gf∗,e(uf (x))).
As for Problem 1, we can obtain a sub-optimal solution Gf,e to Problem 2 by expressing the latter as a supervised learning problem, where the inputs are, once again, sampled according to X and labelled using a reachability oracle. These observations need to be independent from the above introduced training set Zt, i.e., the set used to learn the reachability predictor f .
For e ∈ {pe, f p, f n}, the final rejection rule Rf,e for detecting HA states where the reachability prediction should not be trusted, and thus rejected, is readily obtained by the composition of the uncertainty measure and the error detection rule Rf,e = Gf,e ◦ uf : X → {0, 1}, where Rf,e(x) = 1 if the prediction on state x is rejected; Rf,e(x) = 0, otherwise.
Validation set. As done for the training set, a set Zv is obtained from a sample Xv of X , independent from Xt. Given an uncertainty measure uf , we build a validation set Wve = {(uf (x), 1(e(x))) | x ∈ Xv} which is used to learn Gf,e. The inputs of Wve, referred to as Uv, are the uncertainty measures evaluated on Xv: Uv = {uf (x) | x ∈ Xv}. Each input uf (x) ∈ Uv is then labelled respectively with 1 or 0 depending on whether or not the classifier f makes an error of type e.
A graphical scheme of the full NPM pipeline is presented in 1.
State distribution
+ Reachability oracle
Validation set #
Active Learning Training set "
Neural State Classifier
Uncertainty quantification
Error detection criterion
In the NSC method of [
Bayesian uncertainty measure. Given observations Zt and a BNN fw with w ∼ p(w|Zt), we define the Bayesian uncertainty measure uf : X → U ⊆ R2 as the function mapping inputs x into the empirical mean, μx, and variance, σx2, of the predictive distribution p(yˆ | x, Zt), where yˆ is the class predicted by fw, where w is a sample from the posterior p(w | Zt). Formally, ∀x ∈ X, uf (x) = (μx, σx2).
An unseen input x must have sufficiently low uncertainty values in order for the prediction to be
accepted. We seek to find those uncertainty values that optimally separate the points in Uv – the validation
set – in relation to their classes, that is, separate points yielding errors from those that do not. Optimal
thresholds can be automatically identified by solving an additional supervised learning problem, in this
work we leverage Gaussian Process classification (GPC) [
Active Learning As the accuracy of a classifier increases with the quality and the quantity of observed data, adding samples to Zt will generate a more accurate predictor, and similarly, adding samples to Wv will lead to more precise error detection. Ideally, one wants to maximize accuracy while using the least possible amount of additional samples, because obtaining labeled data is expensive (in NPM, labelling each sample entails solving a reachability checking problem), and the size of the datasets affects the complexity and the dimension of the problem. Therefore, to improve the accuracy of our learning models efficiently, we need a strategy to identify the most “informative” additional samples.
For this purpose, we propose an uncertainty-aware active learning solution, where the re-training points are derived by first sampling a large pool of unlabeled data, and then considering only those points where the current predictor f is still uncertain according to the rejection rule Rf .
Active learning algorithm. We query the HA reachability checker to label the points rejected by Rf and we divide them into two groups: one group is added to the training set Zt, producing the augmented dataset Zta; the other is added to the validation set Zv, producing Zva. The first step consists in retraining the reachability predictor on Zta. Let fa denote the new predictor. The second step requires extracting the augmented validation dataset Wva from Za. To do so, we must first train a new uncertainty measure v ufa so as to reflect the new predictor fa. Then, the new error detection rule Gfa is trained on Wva. In conclusion, this process leads to an updated rejection rule Rfa = Gfa ◦ ufa , which is expected to have a reduced rate of incorrect rejections.
A frequentist approach is also possible [
We experimentally evaluate the proposed method on a benchmark of six hybrid system models with
varying degrees of complexity. We consider four deterministic case studies: the model of the spiking neuron
(SN) action potential [
Evaluation. We consider three configurations: the initial configuration, where the predictor and error detection rules are derived via supervised learning; the active configuration, where the initial models are retrained via our uncertainty-aware active learning; and the passive configuration, where the initial models are retrained using a uniform sampling strategy to augment the dataset and with the same number 1http://dreal.github.io/benchmarks/networks/water/ of observations of the active configuration. In this way, we can evaluate the benefits of employing an uncertainty-based criterion to retrain our models.
Our experimental evaluation demonstrates that our reachability predictors attain high accuracies, consistently above 97.4% and the benefits of active learning are visible from an overall reduction of the rejection rate and an overall increase in the state-classifier accuracy compared to the passive approach. Furthermore, VI scales better than HMC with respect to the dimension of the system and we observe that on average VI outperforms HMC: the initial VI approach yield an NSC accuracy of 98.95%, a rejection rate of 5.19% and a recognition rate of 86.18%. The passive results introduce only minor improvements, whereas active learning yields a significant reduction in the rejection rate (from 5.19% to 2.36%), an increase in the NSC accuracy (from 98.95% to 99.32%) and an increase in the overall recognition rate (from 86.18% to 91.85%).
Initial VI 99.29 95.77 Active VI 99.71 96.55 Passive VI 99.47 100.00
Initial VI 99.58 80.95 Active VI 99.58 85.71 Passive VI 99.71 75.81
Initial VI 99.01 97.98 Active VI 99.84 100.00 Passive VI 99.74 100.00
Initial VI 99.60 77.50 Active VI 99.67 84.85 Passive VI 99.50 75.40
Initial VI 98.14 88.71 Active VI 98.90 92.86 Passive VI 98.66 87.54
Initial VI 98.18 91.21 Active VI 98.20 91.11 Passive VI 98.20 98.52 Rej. rate
Our approach overcomes the computational footprint of reachability checking (infeasible at runtime), while improving on traditional runtime verification by being able to detect future violations in a preemptive way. Among future directions, we plan to extend our approach to support more complex and real-world systems that include noise and partial observability.