Time series classification is a task of paramount importance, as this kind of data often arises in safety-critical applications. However, it is typically tackled with black-box deep learning methods, making it hard for humans to understand the rationale behind their output. To take on this challenge, we propose a neuro-symbolic framework that unifies classification and explanation through direct embedding of trajectories into a space of Signal Temporal Logic (STL) concepts. By introducing a novel STL-inspired kernel that maps raw time series to their alignment with predefined STL formulae, our model jointly optimises for accuracy and interpretability, as each prediction is accompanied by the most relevant logical concepts that characterise it. This enables classification grounded in human-interpretable temporal patterns and produces both local and global symbolic explanations. Early results show competitive performance while offering high-quality logical justifications for model decisions.

In a recent work, Bakhirkin and Basset [3] proposed a new specification language that extends STL. Their logic overcomes the syntactic restrictions of STL, enabling the production and manipulation of real-valued output signals and the expression of properties that have typically been described using other logics, such as STL*. In this contribution, we extend this specification language in three directions. First, we introduce a novel integral operator over sliding windows, allowing the specification of cumulative properties, for example, asserting that the integral of a signal over a time interval remains within a given threshold. Second, we introduce a filtering operator for the sliding window operator, enabling us to restrict the scope of aggregation to signal segments that satisfy the filtering condition. Third, we develop an efficient online monitoring algorithm for the extended logic. Finally, we test the logic on two case studies: an artificial pancreas controller and a monitoring of outdoor weather events.

Modern cyber-physical systems (CPS) can consist of various networked components and agents interacting and communicating with each other. In the context of spatially distributed CPS, these connections can be dynamically dependent on the spatial configuration of the various components and agents. In these settings, robust monitoring of the distributed components is vital to ensuring complex behaviors are achieved, and safety properties are maintained. To this end, we look at defining the automaton semantics for the Spatio-Temporal Reach and Escape Logic (STREL), a formal logic designed to express and monitor spatio-temporal requirements over mobile, spatially distributed CPS. Specifically, STREL reasons about spatio-temporal behavior over dynamic weighted graphs. While STREL is endowed with well defined qualitative and quantitative semantics, in this paper, we propose a novel construction of (weighted) alternating finite automata from STREL specifications that efficiently encodes these semantics. Moreover, we demonstrate how this automaton semantics can be used to perform both, offline and online monitoring for STREL specifications using a simulated drone swarm environment.

Time series classification is a task of paramount importance, as this kind of data often arises in safety-critical applications. However, it is typically tackled with black-box deep learning methods, making it hard for humans to understand the rationale behind their output. To take on this challenge, we propose a novel approach, STELLE (Signal Temporal logic Embedding for Logically-grounded Learning and Explanation), a neuro-symbolic framework that unifies classification and explanation through direct embedding of trajectories into a space of temporal logic concepts. By introducing a novel STL-inspired kernel that maps raw time series to their alignment with predefined STL formulae, our model jointly optimises accuracy and interpretability, as each prediction is accompanied by the most relevant logical concepts that characterise it. This yields (i) local explanations as human-readable STL conditions justifying individual predictions, and (ii) global explanations as class-characterising formulae. Experiments demonstrate that STELLE achieves competitive accuracy while providing logically faithful explanations, validated on diverse real-world benchmarks.

Model checking, which formally verifies whether a system exhibits a certain behaviour or property, is typically tackled by means of algorithms that require the knowledge of the system under analysis. To address this drawback, machine learning model checking has been proposed as a powerful approach for casting the model checking problem as an optimization problem in which a predictor is learnt in a continuous latent space capturing the semantics of formulae. More in detail, a kernel for Signal Temporal Logic (STL) is introduced, so that features of specifications are automatically extracted leveraging the kernel trick. This permits to verify a new formula without the need of accessing a (generative) model of the system, using only a given set of formulae and their satisfaction value, potentially leading to a privacy-preserving method usable to query specifications of a system without giving access to it. This paper investigates the feasibility of this approach quantifying the amount of information leakage due to machine learning model checking on the system that is checked. The analysis is carried out for STL under different training regimes.

We present MoonLight , a tool for monitoring temporal and spatio-temporal properties of mobile, spatially distributed, and interacting entities such as biological and cyber-physical systems. In MoonLight the space is represented as a weighted graph describing the topological configuration in which the single entities are arranged. Both nodes and edges have attributes modeling physical quantities and logical states of the system evolving in time. MoonLight is implemented in Java and supports the monitoring of Spatio-Temporal Reach and Escape Logic (STREL). MoonLight can be used as a standalone command line tool, such as Java API, or via Matlab ™ and Python interfaces. We provide here the description of the tool, its interfaces, and its scripting language using a sensor network and a bike sharing example. We evaluate the tool performances both by comparing it with other tools specialized in monitoring only temporal properties and by monitoring spatio-temporal requirements considering different sizes of dynamical and spatial graphs.

Parameter verification and synthesis problems for stochastic systems are still hard challenges. The tasks become even more prohibitive when the systems are large-scale and the verification/synthesis is respect the satisfaction of some linear temporal logic formulae. In this paper, we review a number of techniques that we designed to tackle such problems. The methods exploit the Gaussian Processes (GP) regression and an efficient Bayesian optimization algorithm.

Type I Diabetes (T1D) is a chronic disease in which the body’s ability to synthesize insulin is destroyed. It can be difficult for patients to manage their T1D, as they must control a variety of behavioral factors that affect glycemic control outcomes. In this paper, we explore T1D patient behaviors using a Signal Temporal Logic (STL) based learning approach. STL formulas learned from real patient data characterize behavior patterns that may result in varying glycemic control. Such logical characterizations can provide feedback to clinicians and their patients about behavioral changes that patients may implement to improve T1D control. We present both individual- and population-level behavior patterns learned from a clinical dataset of 21 T1D patients.

We consider the problem of parametric verification, presenting a recent statistical method to perform parametric verification of linear time properties of stochastic models, estimating the satisfaction probability as a function of model or property parameters. The approach leverages Bayesian Machine Learning based on Gaussian Processes. Under mild conditions on continuity of parameters of the satisfaction probability, it can be shown that property satisfaction is a smooth function of such parameters. Gaussian Processes can effectively capture this smoothness and obtain more-accurate estimates of satisfaction probabilities by transferring information across the parameter space. We leveraged this approach to efficiently solve several tasks, like parameter synthesis, system design, counterexample generation, and requirement synthesis. In this tutorial, we will introduce the basic ideas of the approach and give an overview of the different applications.

Parameterized verification of temporal properties is an active research area, being extremely relevant for model-based design of complex systems. In this paper, we focus on parameter synthesis for stochastic models, looking for regions of the parameter space where the model satisfies a linear time specification with probability greater (or less) than a given threshold. We propose a statistical approach relying on simulation and leveraging a machine learning method based on Gaussian Processes for statistical parametric verification, namely Smoothed Model Checking. By injecting active learning ideas, we obtain an efficient synthesis routine which is able to identify the target regions with statistical guarantees. Our approach, which is implemented in Python, scales better than existing ones with respect to state space of the model and number of parameters. It is applicable to linear time specifications with time constraints and to more complex stochastic models than Markov Chains.

We consider the problem of mining signal temporal logical requirements from a dataset of regular (good) and anomalous (bad) trajectories of a dynamical system. We assume the training set to be labeled by human experts and that we have access only to a limited amount of data, typically noisy. We provide a systematic approach to synthesize both the syntactical structure and the parameters of the temporal logic formula using a two-steps procedure: first, we leverage a novel evolutionary algorithm for learning the structure of the formula; second, we perform the parameter synthesis operating on the statistical emulation of the average robustness for a candidate formula w.r.t. its parameters. We compare our results with our previous work [9] and with a recently proposed decision-tree [8] based method. We present experimental results on two case studies: an anomalous trajectory detection problem of a naval surveillance system and the characterization of an Ineffective Respiratory effort, showing the usefulness of our work.

We introduce a new logic called Signal Convolution Logic (SCL) that combines temporal logic with convolutional filters from digital signal processing. SCL enables to reason about the percentage of time a formula is satisfied in a bounded interval. We demonstrate that this new logic is a suitable formalism to effectively express non-functional requirements in Cyber-Physical Systems displaying noisy and irregular behaviours. We define both a qualitative and quantitative semantics for it, providing an efficient monitoring procedure. Finally, we prove SCL at work to monitor the artificial pancreas controllers that are employed to automate the delivery of insulin for patients with type-1 diabetes.

Search-based testing is widely used to find bugs in models of complex Cyber-Physical Systems. Latest research efforts have improved this approach by casting it as a falsification procedure of formally specified temporal properties, exploiting the robustness semantics of Signal Temporal Logic. The scaling of this approach to highly complex engineering systems requires efficient falsification procedures, which should be applicable also to black box models. Falsification is also exacerbated by the fact that inputs are often time-dependent functions. We tackle the falsification of formal properties of complex black box models of Cyber-Physical Systems, leveraging machine learning techniques from the area of Active Learning. Tailoring these techniques to the falsification problem with time-dependent, functional inputs, we show a considerable gain in computational effort, by reducing the number of model simulations needed. The goodness of the proposed approach is discussed on a challenging industrial-level benchmark from automotive.

The design of genetic or protein networks that satisfy a given set of behavioural specifications is one of the main challenges of synthetic biology. Model-based design is a natural choice in this respect. Here we consider the problem of tuning parameters of a stochastic model to force one or more behavioural goals to hold. In particular, we consider several objectives specified by signal temporal logic formulae, and we look for a parameter set making their satisfaction probability as large as possible. This formalisation results in a multi-objective optimisation problem, which we solve by considering an optimisation scheme combining satisfaction probability and average robustness of STL properties, leveraging state of the art multi-objective optimisation routines.