Hagen Heermann

• This dissertation introduces two novel approaches that combine Runtime Verification and Anomaly Detection to detect deviations from expected system behavior. Within this hybrid framework, the primary goals are twofold: ensuring correctness with respect to a given specification—specifically, a dynamical model—and maintaining simplicity in the classification process. The first approach utilizes reachability analysis through Affine Arithmetic Decision Diagrams (AADDs) and Affine Binary Decision Diagrams (BDDAs) within symbolic sim- ulations. These diagrams rely on affine forms, which represent uncertainty using linear expressions with noise symbols. To manage complexity and provide a structured represen- tation of the state space, the Affine Arithmetic Cartesian Decision Diagram (AACDD) was introduced. The AACDD merges all AADDs and BDDAs into a single structure, capturing all valid state tuples by encoding the relationships between continuous and discrete state variables. This unified representation enables a systematic evaluation of whether observed state transitions conform to the expected dynamics. Within this frame- work, system behavior is evaluated by checking whether observed state transitions (both continuous and discrete) conform to the expected dynamics. This evaluation is formal- ized through consistency conditions, which ensure that (i) transitions between continuous states satisfy specific inequalities (continuous consistency) and (ii) transitions between discrete states follow predefined logical patterns (discrete consistency). These conditions are expressed as systems of inequalities over noise symbols, and a simplex solver is used to determine whether a feasible solution exists. Building on this foundation, the second approach, termed the H-Classifier, simplifies the evaluation process by transforming the inequality systems into the transition space, which directly represents the system’s state transitions from time k to k+1. A key advantage of this transformation is that observed measurements no longer need to be interpreted by solving for feasible solutions; instead, they can be directly evaluated by substituting them into the corresponding inequality systems. While the initial approach ensures strong correctness, its reliance on a simplex solver introduces significant com- putational demands. In contrast, the H-Classifier, though slightly imperfect in certain cases, offers a highly efficient classification process by leveraging direct evaluation within the transition space. The results indicate that while neither approach is flawless, both come close to meeting the initial goals of correctness relative to the dynamical model and simple classification. The dissertation concludes with a discussion on potential future work, including scaling the approaches to more complex systems, deploying them in Digital Twin environments, and further refining the H-Classifier for formal correctness. Additionally, the rich infor- mation encoded in the model-based approach could be leveraged for multi-class classifi- cation and to enhance the explainability of the system, paving the way for applications in predictive maintenance.