Time-critical systems must satisfy temporal constraints whose correctness depends not only on event ordering but also on precise timing. Metric Interval Temporal Logic (MITL) provides a formalism to express such requirements. Although robustness has been widely studied under signal-based interpretations, it remains largely unexplored for point-based semantics, where executions are sequences of timestamped facts. In this setting, small timing variations may arbitrarily change Boolean satisfaction, revealing the instability of temporal truth under uncertainty. We introduce a notion of time robustness for MITL over point-based semantics, interpreting robustness as a margin of validity of temporal interpretations. We define a quantitative semantics and prove soundness with respect to Boolean satisfaction together with a Lipschitz stability property with respect to timestamp perturbations, which induces a metric notion of proximity between interpretations. The semantics admits a polynomial-time evaluation procedure and is illustrated on two case studies (drone surveillance and smart hospital), where robustness empirically correlates with tolerance to temporal noise.

We consider the problem of predictive monitoring (PM), i.e., predicting at runtime the satisfaction of a desired property from the current system’s state. Due to its relevance for runtime safety assurance and online control, PM methods need to be efficient to enable timely interventions against predicted violations, while providing correctness guarantees. We introduce quantitative predictive monitoring (QPM), the first PM method to support stochastic processes and rich specifications given in Signal Temporal Logic (STL). Unlike most of the existing PM techniques that predict whether or not some property ϕ is satisfied, QPM provides a quantitative measure of satisfaction by predicting the quantitative (aka robust) STL semantics of ϕ. QPM derives prediction intervals that are highly efficient to compute and with probabilistic guarantees, in that the intervals cover with arbitrary probability the STL robustness values relative to the stochastic evolution of the system. To do so, we take a machine-learning approach and leverage recent advances in conformal inference for quantile regression, thereby avoiding expensive Monte Carlo simulations at runtime to estimate the intervals. We also show how our monitors can be combined in a compositional manner to handle composite formulas, without retraining the predictors or sacrificing the guarantees. We demonstrate the effectiveness and scalability of QPM over a benchmark of four discrete-time stochastic processes with varying degrees of complexity.

Abstract Neural state classification (NSC) is a recently proposed method for runtime predictive monitoring of hybrid automata (HA) using deep neural networks (DNNs). NSC trains a DNN as an approximate reachability predictor that labels an HA state x as positive if an unsafe state is reachable from x within a given time bound, and labels x as negative otherwise. 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. We develop two versions of NPM based, respectively, on the use of frequentist and Bayesian techniques to learn the predictor and the rejection rule. Both versions are highly efficient, with computation times on the order of milliseconds, and effective, managing in our experimental evaluation to successfully reject almost all incorrect predictions. In our experiments on a benchmark suite of six hybrid systems, we found that the frequentist approach consistently outperforms the Bayesian one. We also observed that the Bayesian approach is less practical, requiring a careful and problem-specific choice of hyperparameters.

The glycemia regulation is a significant challenge in the Artificial Pancreas (AP) scenario. Several control systems have been developed in the last years, many of them requiring meal announcements. Therefore, if the patients skip the meal announcement or make a mistake in the estimation of the amount of carbohydrates, the control performance will be negatively affected. In this extended version of our previous work, we present a Model Predictive Controller (MPC) for the AP in which the meal is treated as a disturbance to be estimated by an Unknown Input Observer (UIO). The MPC constraints are expressed in terms of Signal Temporal Logic (STL) specifications. Indeed, in the AP some requirements result in hard constraints (in particular, absolutely avoid hypoglycemia and absolutely avoid severe hyperglycemia) and some other in soft constraints (avoid a prolonged hyperglycemia) and STL is suitable for expressing such requirements. The achieved results are obtained using the BluSTL toolbox, which allows to synthesize model predictive controllers with STL constraints. We report simulations showing that the proposed approach, avoiding unnecessary restrictions, provides safe trajectories in correspondence of higher unknown disturbance.

We consider a drug infusion scenario in which a drug is delivered through an infusion pump to a patient, whose vital parameters are monitored via a bedside monitor. Drug infusion therapies are based on clinical protocols that are drug-specific and very diversified. The burden of their proper application on several patients lies, most of the times, on nursing staff alone. With the aim of making the choices safe and prompt and limiting human errors, we build a system that suggests the proper action based on the protocol and the status of the patient. Given the high variability of protocols, it is important to choose a flexible structure. We choose Hierarchical Colored Petri Nets (HCPN), a mathematical formalism for describing discrete event dynamic systems, which is, in fact, modular, expressive and admits a graphic representation. Cancer infusion therapy is the case study considered, as that clinical scenario is likely to become critical from a staff/patient ratio point of view, since the number of patients is continuously growing.

Insulin is a peptide hormone produced by the pancreas to regulate the cells intake of glucose in the blood. Type 1 diabetes compromises this particular capacity of the pancreas. Patients with this disease inject insulin to regulate the level of glucose in the blood, thus reducing the risk of longterm complications. Artificial Pancreas (AP) is a wearable device developed to provide automatic delivery of insuline, allowing a potentially significant improvement in the quality of life of patients. In this paper we apply to the AP a Model Predictive Controller able to generate state trajectories that meet constraints expressed through Signal Temporal Logic (STL). Such a form of constraints is indeed appropriate for the AP, in which some requirements result in hard constraints (absolutely avoid hypoglycaemia) and some other in soft constraints (avoid a prolonged hyperglycaemia). We rely on the BluSTL toolbox, which allows to automatically generate controllers using STL specifications. We perform simulations on two different scenarios: an MPC controller that uses the same constraints as [1] and an MPC-STL controller in both deterministic and adversarial environment (robust control). We show that the soft constraints permitted by STL avoid unnecessary restriction, providing safe trajectories in correspondence of higher disturbance.