Specification Mining for Cyber-Physical Systems

Cyber-Physical Systems (CPS) are widely used complex systems that integrate computational and physical components, enabling continuous interaction with the real-world environment. In recent years, the integration of Machine Learning components has given rise to learning-enabled CPS, allowing them to operate autonomously. CPS applications span various domains, including self-driving vehicles, medical devices, smart cities, robotic systems, and smart grids.
As CPS grow in complexity, ensuring their trustworthiness has become increasingly challenging but remains essential for their adoption, especially in safety-critical domains.
In this context, formal specifications are crucial for expressing requirements on system behavior in a precise and unambiguous way. Additionally, their mathematical structure enables the automation of runtime verification techniques –such as monitoring, runtime enforcement, and falsification– which provide rigorous yet scalable methods for verifying system executions. Despite their importance, formal specifications are often unavailable
because manually defining them is challenging due to system complexity and unpredictable environments. Specification mining addresses this issue as it is the research field dedicated to automatically inferring system properties from its executions and interactions with the environment.
In this thesis, we address several research gaps in specification mining for CPS. Specifically, we focus on Signal Temporal Logic (STL), a popular formalism for expressing temporal properties of CPS in a rigorous yet human-understandable manner, and its extensions.
We introduce a method for learning STL specifications that can predict safety violations in advance based only on variables that are observable by the system, thus allowing the autonomous assessment of its safety at runtime. Moreover, we propose a new technique for learning parameter values for STL formulas to perform multi-class classification of system executions, which is essential, for instance, in recognizing different system failures simultaneously. We then develop the first method for mining STL hyperproperties, which enhance the expressiveness of properties by capturing relationships across multiple
system executions. Finally, we focus on the shape of the executions and extract formal specifications to characterize their geometric patterns, which are particularly useful for analyzing time-series data with repeated patterns, such as cardiac activity or voltage signals. We evaluate the performance of each proposed method on several case studies, as well as the interpretability of the learned formulas.