Colloquium on Design and Verification of Cyber-Physical Systems: From Theory to Applications
On the occasion of Martin Fränzle's 60th birthday in October 2024, there has been a colloquium to honour his achievements and personal commitment to the scientific community during the past decades.
The colloquium took place on Friday, 28 February 2025 in the assembly hall of the Carl von Ossietzky Universität Oldenburg in Oldenburg, Germany. In the evening, the colloquium concluded with a dinner to which Martin and Barbara cordially invited.
The musical programme was performed by Andreas Peter on the grand piano.
Programme
Registration
08:30
Session 1
09:00
Andreas Rauh
Opening
09:15
Werner Damm, Christoph Herrmann
Human Cyber-Physical Systems: Safety Acceptance, Social and Cultural Embeddedness
J. Adelt, M. Farrell, P. Herber, M. Luckcuck, and R. Monahan, "Defining Contracts for Autonomous Hybrid Systems in Structured Natural Language" , Rauh, A., Finkbeiner, B., and Kröger, P. Eds., Cham: Springer Nature Switzerland.
doi: 10.1007/978-3-032-16855-9_13
@InBook{adelt:mf60, pages = {297--319},
title = {Defining Contracts for Autonomous Hybrid Systems in Structured Natural Language},
publisher = {Springer Nature Switzerland},
year = {2026},
author = {Adelt, Julius and Farrell, Marie and Herber, Paula and Luckcuck, Matt and Monahan, Rosemary},
editor = {Rauh, Andreas and Finkbeiner, Bernd and Kr{\"o}ger, Paul},
address = {Cham},
isbn = {978-3-032-16855-9},
abstract = {In the era of self-driving vehicles and highly autonomous distributed control systems, hybrid systems increasingly use machine learning techniques to make good control decisions in unexpected situations. These systems are often safety-critical, making the application of formal methods to ensure their correctness highly desirable. However, building formal specifications is time-consuming and requires high expertise. In this paper, we present an approach for the definition in structured natural language of formal specifications as they are required for deductive verification of autonomous hybrid systems. To achieve this we extend the Formal Requirements Elicitation Tool (FRET) with templates that support reusable contracts for intelligent hybrid systems. FRET then helps to derive differential dynamic logic (d{\$}{\$}{\backslash}mathcal {\{}L{\}}{\$}{\$}L) properties and contracts from the requirements written in structured natural language using these templates. The resulting dL specifications can be used both for the deductive verification of a given intelligent hybrid system under the assumption that learning components adhere to their contracts, and to enforce safe actions at runtime. We demonstrate the applicability of our approach with several case studies. We show that the necessary properties and contracts can be derived using our FRET templates.},
booktitle = {Design and Verification of Cyber-Physical Systems: From Theory to Applications: Essays Dedicated to Martin Fr{\"a}nzle on the Occasion of His 60th Birthday},
doi = {10.1007/978-3-032-16855-9_13},
url = {https://doi.org/10.1007/978-3-032-16855-9_13},
}
A. Amrane, H. Bazille, E. Clement, U. Fahrenberg, and P. Schlehuber-Caissier, "Higher-Dimensional Timed Automata for Real-Time Concurrency" , Rauh, A., Finkbeiner, B., and Kröger, P. Eds., Cham: Springer Nature Switzerland.
doi: 10.1007/978-3-032-16855-9_4
@InBook{amrane:mf60, pages = {66--100},
title = {Higher-Dimensional Timed Automata for Real-Time Concurrency},
publisher = {Springer Nature Switzerland},
year = {2026},
author = {Amrane, Amazigh and Bazille, Hugo and Clement, Emily and Fahrenberg, Uli and Schlehuber-Caissier, Philipp},
editor = {Rauh, Andreas and Finkbeiner, Bernd and Kr{\"o}ger, Paul},
address = {Cham},
isbn = {978-3-032-16855-9},
abstract = {We present a new language semantics for real-time concurrency. Its operational models are higher-dimensional timed automata (HDTAs), a generalization of both higher-dimensional automata and timed automata. In real-time concurrent systems, both concurrency of events and timing and duration of events are of interest. Thus, HDTAs combine the non-interleaving concurrency model of higher-dimensional automata with the real-time modeling, using clocks, of timed automata. We define languages of HDTAs as sets of interval-timed pomsets with interfaces.},
booktitle = {Design and Verification of Cyber-Physical Systems: From Theory to Applications: Essays Dedicated to Martin Fr{\"a}nzle on the Occasion of His 60th Birthday},
doi = {10.1007/978-3-032-16855-9_4},
url = {https://doi.org/10.1007/978-3-032-16855-9_4},
}
F. Bruns, A. Rauh, and M. Fnadi, "Set-Based Assumption-Guarantee Reasoning for Handling Uncertainty in Functionality and Safety Verification of Dynamic Systems" , Rauh, A., Finkbeiner, B., and Kröger, P. Eds., Cham: Springer Nature Switzerland.
doi: 10.1007/978-3-032-16855-9_14
@InBook{bruns:mf60, pages = {320--347},
title = {Set-Based Assumption-Guarantee Reasoning for Handling Uncertainty in Functionality and Safety Verification of Dynamic Systems},
publisher = {Springer Nature Switzerland},
year = {2026},
author = {Bruns, Friederike and Rauh, Andreas and Fnadi, Mohamed},
editor = {Rauh, Andreas and Finkbeiner, Bernd and Kr{\"o}ger, Paul},
address = {Cham},
isbn = {978-3-032-16855-9},
abstract = {The increasing complexity of Cyber-Physical Systems (CPSs), particularly in safety-critical applications, necessitates advanced methods for design and verification. Modern CPSs must operate reliably in uncertain environments characterized by noise, external disturbances, and dynamic conditions. Addressing these challenges requires methodologies that are capable of capturing both internal system complexities and external uncertainties. Assumption-Guarantee reasoning, often expressed using temporal logics, provides a modular framework for verification. However, current temporal logics are limited in their ability to effectively handle uncertainties. This paper introduces Set-Based Temporal Logic (SBTL) as a solution to these limitations by extending traditional contract specifications to incorporate a set-based reachability analysis, which enables a more detailed representation of uncertainty and accommodates for implicit system behaviors. By integrating set-based reasoning with temporal constraints, SBTL offers a more expressive and robust specification formalism. The approach is demonstrated through simulations of a DC motor-based drive train operating in an uncertain and dynamic environment, featuring a combined state and disturbance estimator. Results highlight the enhanced robustness of the closed-loop control system, ensuring consistent disturbance reconstruction and alignment of system trajectories with desired behavior.},
booktitle = {Design and Verification of Cyber-Physical Systems: From Theory to Applications: Essays Dedicated to Martin Fr{\"a}nzle on the Occasion of His 60th Birthday},
doi = {10.1007/978-3-032-16855-9_14},
url = {https://doi.org/10.1007/978-3-032-16855-9_14},
}
H. Dayekh, N. Basset, and T. Dang, "Learning of Switched Nonlinear Dynamical Systems: Passive and Active Approaches" , Rauh, A., Finkbeiner, B., and Kröger, P. Eds., Cham: Springer Nature Switzerland.
doi: 10.1007/978-3-032-16855-9_9
@InBook{dayekh:mf60, pages = {198--222},
title = {Learning of Switched Nonlinear Dynamical Systems: Passive and Active Approaches},
publisher = {Springer Nature Switzerland},
year = {2026},
author = {Dayekh, Hadi and Basset, Nicolas and Dang, Thao},
editor = {Rauh, Andreas and Finkbeiner, Bernd and Kr{\"o}ger, Paul},
address = {Cham},
isbn = {978-3-032-16855-9},
abstract = {Identification of hybrid systems is a well-researched topic, with most techniques relying on passive learning. Despite the abundance of data, active learning and counterexample-guided improvement of learned hybrid systems remain less explored. We present a passive and an active approach for the identification of state-dependent switched nonlinear systems with continuous state variables. We use segmentation in both of our approaches. Our passive approach consists of solving an optimization problem over a fixed set of data to find the continuous dynamics of the system-under-learning and the modes of training data, assuming a known number of modes, while our active approach incrementally learns these dynamics and mode information with no previous assumption on the number of modes. We showcase both of our approaches in a set of experiments, as well as a case study on electrical circuits.},
booktitle = {Design and Verification of Cyber-Physical Systems: From Theory to Applications: Essays Dedicated to Martin Fr{\"a}nzle on the Occasion of His 60th Birthday},
doi = {10.1007/978-3-032-16855-9_9},
url = {https://doi.org/10.1007/978-3-032-16855-9_9},
}
J. Ding, T. Wu, Y. Qian, L. Zhang, S. A. Deka, and B. Xue, "Provable Reach-Avoid Controllers Synthesis for Deterministic Discrete-Time Systems Based on Convex Computations of Controlled Reach-Avoid Sets" , Rauh, A., Finkbeiner, B., and Kröger, P. Eds., Cham: Springer Nature Switzerland.
doi: 10.1007/978-3-032-16855-9_10
@InBook{ding:mf60, pages = {223--243},
title = {Provable Reach-Avoid Controllers Synthesis for Deterministic Discrete-Time Systems Based on Convex Computations of Controlled Reach-Avoid Sets},
publisher = {Springer Nature Switzerland},
year = {2026},
author = {Ding, Jianqiang and Wu, Taoran and Qian, Yuping and Zhang, Lijun and Deka, Shankar A. and Xue, Bai},
editor = {Rauh, Andreas and Finkbeiner, Bernd and Kr{\"o}ger, Paul},
address = {Cham},
isbn = {978-3-032-16855-9},
abstract = {In this paper, we present a novel approach for synthesizing provable reach-avoid controllers. Our approach focuses on driving a deterministic discrete-time system, operating in an unknown environment, to safely reach a desired target set. Within the reachability analysis framework, we propose a method based on convex computation of inner-approximations of controlled reach-avoid sets (CRSs). The controlled reach-avoid set represents the set of states from which the system can enter the target set while remaining inside the safe set before the target hitting time. By defining the boundary of the CRS as a barrier, we effectively separate states that can achieve the reach-avoid objective from those that cannot. Thus, the computed inner-approximation provides a viable space for the system to accomplish the reach-avoid objective. Our approach for synthesizing reach-avoid controllers involves three main steps. Firstly, we employ a support vector machine approach to learn a safe set of states in the unknown environment using sensor measurements. Secondly, based on the learned safe set and target set, we compute an inner-approximation of the CRS by solving a convex optimization problem. Finally, we synthesize controllers online to ensure that the system evolves within the computed inner-approximation, ultimately reaching the target set. To illustrate the effectiveness of our proposed method, we demonstrate its application on a Dubin's car system.},
booktitle = {Design and Verification of Cyber-Physical Systems: From Theory to Applications: Essays Dedicated to Martin Fr{\"a}nzle on the Occasion of His 60th Birthday},
doi = {10.1007/978-3-032-16855-9_10},
url = {https://doi.org/10.1007/978-3-032-16855-9_10},
}
M. Farsang, S. A. Neubauer, and R. Grosu, "Liquid Resistance Liquid Capacitance Networks" , Rauh, A., Finkbeiner, B., and Kröger, P. Eds., Cham: Springer Nature Switzerland.
doi: 10.1007/978-3-032-16855-9_11
@InBook{farsang:mf60, pages = {244--272},
title = {Liquid Resistance Liquid Capacitance Networks},
publisher = {Springer Nature Switzerland},
year = {2026},
author = {Farsang, M{\'o}nika and Neubauer, Sophie A. and Grosu, Radu},
editor = {Rauh, Andreas and Finkbeiner, Bernd and Kr{\"o}ger, Paul},
address = {Cham},
isbn = {978-3-032-16855-9},
abstract = {We introduce liquid-resistance liquid-capacitance neural networks (LRCs), a neural-ODE model which considerably improves the generalization, accuracy, and biological plausibility of electrical equivalent circuits (EECs), liquid time-constant networks (LTCs), and saturated liquid time-constant networks (STCs), respectively. We also introduce LRC units (LRCUs), as a very efficient and accurate gated RNN-model, which results from solving LRCs with an explicit Euler scheme using just one unfolding. We empirically show and formally prove that the liquid capacitance of LRCs considerably dampens the oscillations of LTCs and STCs, while at the same time dramatically increasing accuracy even for cheap solvers. We experimentally demonstrate that LRCs are a highly competitive alternative to popular neural ODEs and gated RNNs in terms of accuracy, efficiency, and interpretability, on classic time-series benchmarks and a complex autonomous-driving lane-keeping task.},
booktitle = {Design and Verification of Cyber-Physical Systems: From Theory to Applications: Essays Dedicated to Martin Fr{\"a}nzle on the Occasion of His 60th Birthday},
doi = {10.1007/978-3-032-16855-9_11},
url = {https://doi.org/10.1007/978-3-032-16855-9_11},
}
B. Finkbeiner and F. Kohn, "Precision in the Presence of Uncertainty: SMT-Based Runtime Validation of CPS" , Rauh, A., Finkbeiner, B., and Kröger, P. Eds., Cham: Springer Nature Switzerland.
doi: 10.1007/978-3-032-16855-9_22
@InBook{finkbeiner:mf60, pages = {520--542},
title = {Precision in the Presence of Uncertainty: SMT-Based Runtime Validation of CPS},
publisher = {Springer Nature Switzerland},
year = {2026},
author = {Finkbeiner, Bernd and Kohn, Florian},
editor = {Rauh, Andreas and Finkbeiner, Bernd and Kr{\"o}ger, Paul},
address = {Cham},
isbn = {978-3-032-16855-9},
abstract = {We study the offline monitoring problem for stream-based specifications of cyber-physical systems. A stream-based monitor translates streams of input data, such as sensor readings, into streams of aggregate statistics and verdicts about the safety of the system. Since physical sensors are prone to measurement noise and errors, it becomes necessary to track the uncertainty in the processing and aggregation steps within the monitor. In previous joint work with Martin Fr{\"a}nzle and Paul Kr{\"o}ger, we proposed RLola, an extension of the stream-based language Lola [8] with slack variables that capture this uncertainty, and an online monitoring algorithm for a fragment of RLola. This paper introduces an offline monitoring algorithm for RLola based on satisfiability modulo theories (SMT). While the online algorithm evaluates boolean trigger conditions one at a time, verifying the existence of a hypothetical ground-truth trace that avoids the trigger condition at the current time step, offline monitoring assumes that the complete system trace is given: the offline algorithm then verifies the existence of a hypothetical ground-truth trace that avoids the trigger conditions across all time-steps. As a result, the offline algorithm can identify trigger violations that the online algorithm fails to detect. We evaluate the algorithm's precision and running time using an example, comparing it to the existing online monitoring algorithm.},
booktitle = {Design and Verification of Cyber-Physical Systems: From Theory to Applications: Essays Dedicated to Martin Fr{\"a}nzle on the Occasion of His 60th Birthday},
doi = {10.1007/978-3-032-16855-9_22},
url = {https://doi.org/10.1007/978-3-032-16855-9_22},
}
Y. Gao, C. Zhou, D. Zanarini, D. Bresolin, K. H. Johansson, and A. Abate, "Sampling-Based Polytope Calculus: Computations and Applications" , Rauh, A., Finkbeiner, B., and Kröger, P. Eds., Cham: Springer Nature Switzerland.
doi: 10.1007/978-3-032-16855-9_3
@InBook{gao:mf60, pages = {48--65},
title = {Sampling-Based Polytope Calculus: Computations and Applications},
publisher = {Springer Nature Switzerland},
year = {2026},
author = {Gao, Yulong and Zhou, Can and Zanarini, Davide and Bresolin, Davide and Johansson, Karl H. and Abate, Alessandro},
editor = {Rauh, Andreas and Finkbeiner, Bernd and Kr{\"o}ger, Paul},
address = {Cham},
isbn = {978-3-032-16855-9},
abstract = {Polytope calculus refers to the computation of polytopes under set operations and to algorithms for the conversion across their different representations. It is fundamental for, among other uses, reachability analysis of dynamical systems and thus, more generally, verification approaches for hybrid dynamical models. However, tackling the computational complexities inherent in polytope calculus poses challenges, since most operations exhibit exponential time complexity. In this paper, we introduce novel sampling-based algorithms to compute V-polytope representations, which provide efficient polynomial-time solutions with high approximation accuracy for common operations in polytope calculus. We show the soundness and probabilistic tightness of the sample-based approach. Following a comprehensive evaluation, we highlight the superior performance of the proposed algorithms in comparison to existing approaches, both in terms of scalability and approximation quality. We further develop a new verification-based method to compute an under-approximate H-polytope from a V-polytope representation, which complements the sampling-based algorithm for polytope calculus. We finally showcase their practical relevance in case studies concerning computation of invariant sets and reachability analysis for dynamical systems, thus demonstrating the effectiveness of the proposed approach.},
booktitle = {Design and Verification of Cyber-Physical Systems: From Theory to Applications: Essays Dedicated to Martin Fr{\"a}nzle on the Occasion of His 60th Birthday},
doi = {10.1007/978-3-032-16855-9_3},
url = {https://doi.org/10.1007/978-3-032-16855-9_3},
}
C. Herde, T. Teige, A. Eggers, and K. Scheibler, "Boolean Dreams and Real Constraints: Two Decades of iSAT Solving the Undecidable" , Rauh, A., Finkbeiner, B., and Kröger, P. Eds., Cham: Springer Nature Switzerland.
doi: 10.1007/978-3-032-16855-9_18
@InBook{herde:mf60, pages = {429--444},
title = {Boolean Dreams and Real Constraints: Two Decades of iSAT Solving the Undecidable},
publisher = {Springer Nature Switzerland},
year = {2026},
author = {Herde, Christian and Teige, Tino and Eggers, Andreas and Scheibler, Karsten},
editor = {Rauh, Andreas and Finkbeiner, Bernd and Kr{\"o}ger, Paul},
address = {Cham},
isbn = {978-3-032-16855-9},
abstract = {In this paper, we recount the story of iSAT, one of the tools we developed and explored during our doctoral studies. iSAT is a solver that builds on a synthesis of DPLL SAT solving and interval constraint solving, leveraging the algorithmic commonalities between these two techniques to create a unified approach. It addresses Boolean combinations of theory atoms from the undecidable theory of nonlinear arithmetic constraints over the reals and integers, including transcendental functions. What distinguishes iSAT is that, unlike many other academic tools that end up shelved after serving their research purpose, it has evolved from its academic origins 20 years ago to become one of the backend engines of a commercial software product for the automated testing and verification of embedded systems. Over the years, we developed and investigated various algorithmic enhancements to the solver core and explored multiple extensions. Notably, we added native support for handling ordinary differential equations and extended iSAT to handle stochastic constraint systems involving stochastic quantifiers. We developed iSAT while working under the guidance of our doctoral advisor, Martin Fr{\"a}nzle, in whose honor we are writing this paper for his 60th birthday. Thus, this story is also a reflection of the years we spent with Martin, a time we remember fondly.},
booktitle = {Design and Verification of Cyber-Physical Systems: From Theory to Applications: Essays Dedicated to Martin Fr{\"a}nzle on the Occasion of His 60th Birthday},
doi = {10.1007/978-3-032-16855-9_18},
url = {https://doi.org/10.1007/978-3-032-16855-9_18},
}
Z. Hou, H. Zhu, and J. P. Bowen, "Operational and Algebraic Approaches to the Two-Run Relational System" , Rauh, A., Finkbeiner, B., and Kröger, P. Eds., Cham: Springer Nature Switzerland.
doi: 10.1007/978-3-032-16855-9_7
@InBook{hou:mf60, pages = {150--170},
title = {Operational and Algebraic Approaches to the Two-Run Relational System},
publisher = {Springer Nature Switzerland},
year = {2026},
author = {Hou, Zhiru and Zhu, Huibiao and Bowen, Jonathan P.},
editor = {Rauh, Andreas and Finkbeiner, Bernd and Kr{\"o}ger, Paul},
address = {Cham},
isbn = {978-3-032-16855-9},
abstract = {Relational Hoare logic extends the applicability of modular deductive verification to encompass the verification of crucial 2-run properties. Most of the current research mainly focuses on the practical applications of relational Hoare logic. However, incorporating parallel programs into the logic may further complicate the system design, which is an aspect that most research has overlooked. Therefore, this paper updates the system, referred to as the relational system, by incorporating parallel composition. In this paper, we formalize an operational semantics (called relational operational semantics) for the system, which provides a precise understanding of the language and further explores the implications of 2-runs from the formal methods perspective. In order to investigate program equivalence, bisimulation is introduced for the relational system based on the operational semantics. Furthermore, a set of algebraic laws is studied, which includes the conditional construct and parallel composition. The correctness of these algebraic laws is proved via the defined bisimulation. This reflects that our bisimulation is a practical approach to exploring program equivalence for the system.},
booktitle = {Design and Verification of Cyber-Physical Systems: From Theory to Applications: Essays Dedicated to Martin Fr{\"a}nzle on the Occasion of His 60th Birthday},
doi = {10.1007/978-3-032-16855-9_7},
url = {https://doi.org/10.1007/978-3-032-16855-9_7},
}
J. Kovács, E. Ábrahám, M. Niehage, and A. Remke, "Martin: A Novel Mechanism for Rate Adaption in Continuous Petri Nets" , Rauh, A., Finkbeiner, B., and Kröger, P. Eds., Cham: Springer Nature Switzerland.
doi: 10.1007/978-3-032-16855-9_8
@InBook{kovacs:mf60, pages = {173--197},
title = {Martin: A Novel Mechanism for Rate Adaption in Continuous Petri Nets},
publisher = {Springer Nature Switzerland},
year = {2026},
author = {Kov{\'a}cs, J{\'o}zsef and {\'A}brah{\'a}m, Erika and Niehage, Mathis and Remke, Anne},
editor = {Rauh, Andreas and Finkbeiner, Bernd and Kr{\"o}ger, Paul},
address = {Cham},
isbn = {978-3-032-16855-9},
abstract = {For the modeling and evaluation of fluid systems, continuous Petri nets offer a suitable formalism. Continuous places, modeling fluid storage, can be connected using continuous transitions, which model fluid transportation with their specified nominal flow rates. During the evolution of such systems, the fluid levels in continuous places evolve continuously, and places with less in- than outflow can get empty. To remain physically meaningful in such conflicted cases, the semantics reduces the outflow rates to match the inflow, in a process called rate adaption. For the computation of the rate adaption results during simulation or analysis, the state-of-the-art approach is to reduce the outflow rates for single conflicted empty places in a certain fixed order. However, the termination and physical meaningfulness of this greedy rate adaption method could be guaranteed only for a strongly restricted model class.},
booktitle = {Design and Verification of Cyber-Physical Systems: From Theory to Applications: Essays Dedicated to Martin Fr{\"a}nzle on the Occasion of His 60th Birthday},
doi = {10.1007/978-3-032-16855-9_8},
url = {https://doi.org/10.1007/978-3-032-16855-9_8},
}
Z. Li, M. Yang, S. Feng, and M. Chen, "Fixed-Point Reasoning for Stochastic Systems" , Rauh, A., Finkbeiner, B., and Kröger, P. Eds., Cham: Springer Nature Switzerland.
doi: 10.1007/978-3-032-16855-9_5
@InBook{li:mf60, pages = {101--125},
title = {Fixed-Point Reasoning for Stochastic Systems},
publisher = {Springer Nature Switzerland},
year = {2026},
author = {Li, Zhiyang and Yang, Mingqi and Feng, Shenghua and Chen, Mingshuai},
editor = {Rauh, Andreas and Finkbeiner, Bernd and Kr{\"o}ger, Paul},
address = {Cham},
isbn = {978-3-032-16855-9},
abstract = {Fixed points are mathematical objects that are commonly employed in computer science to characterize key properties of iterative or cyclic behaviors, e.g., unbounded loops and recursions in programs or cycles in transition systems. Reasoning about such behaviors is arguably the hardest task in formal verification. The problem is even harder for stochastic systems as it often amounts to inferring quantitative fixed points that are highly intractable in practice. This article surveys recent advancements in fixed-point reasoning for stochastic systems modeled as probabilistic programs, probabilistic transition systems, and stochastic hybrid systems and outlines potential directions for future research thereof. The core of our results is the fixed-point reasoning landscape for stochastic systems, where we focus on formal techniques that either (i) establish sound over-/under-approximations of quantitative fixed points; or (ii) infer the exact fixed points for a restricted class of systems.},
booktitle = {Design and Verification of Cyber-Physical Systems: From Theory to Applications: Essays Dedicated to Martin Fr{\"a}nzle on the Occasion of His 60th Birthday},
doi = {10.1007/978-3-032-16855-9_5},
url = {https://doi.org/10.1007/978-3-032-16855-9_5},
}
G. Lin, H. Wu, and N. Zhan, "Barrier Certificate Synthesis via Interpolation and Difference-of-Convex Programming" , Rauh, A., Finkbeiner, B., and Kröger, P. Eds., Cham: Springer Nature Switzerland.
doi: 10.1007/978-3-032-16855-9_12
@InBook{lin:mf60, pages = {273--293},
title = {Barrier Certificate Synthesis via Interpolation and Difference-of-Convex Programming},
publisher = {Springer Nature Switzerland},
year = {2026},
author = {Lin, Guanhua and Wu, Hao and Zhan, Naijun},
editor = {Rauh, Andreas and Finkbeiner, Bernd and Kr{\"o}ger, Paul},
address = {Cham},
isbn = {978-3-032-16855-9},
abstract = {Barrier certificates play a crucial role in the verification of cyber-physical systems (CPS), particularly in safety-critical scenarios. The underlying principle involves encoding the conditions for a polynomial's zero sub-level set to be a differential invariant, enabling the application of powerful mathematical optimization techniques. A primary challenge in this approach is that, in general settings, the resulting constraints are non-convex and lack efficient solvers. To address this issue, Wang et al. [48, 49] proposed a difference-of-convex (DC) algorithm to approximate a non-convex program by solving a series of convex programs using semidefinite programming (SDP). While this approach offers a guarantee on convergence to local optimums, it suffers from the initial value problem. In this paper, we try to solve this problem based on the key insight that a user-defined polynomial in barrier certificate conditions should be selected to be an interpolant separating the initial region and the unsafe region. A novel approach is proposed to adjust the position of the interpolant via SDP, and the obtained interpolant is fed into the DC algorithm as the initial value. Experiments show that our strategy can significantly improve the performance of the DC algorithm.},
booktitle = {Design and Verification of Cyber-Physical Systems: From Theory to Applications: Essays Dedicated to Martin Fr{\"a}nzle on the Occasion of His 60th Birthday},
doi = {10.1007/978-3-032-16855-9_12},
url = {https://doi.org/10.1007/978-3-032-16855-9_12},
}
R. L. Tagne Mogue, N. Meslem, Y. Becis-Aubry, E. Courtial, and N. Ramdani, "Secure Set-Based State Estimation of Multi-sensor Switched Systems: An Impulsive-Switched Observer Approach" , Rauh, A., Finkbeiner, B., and Kröger, P. Eds., Cham: Springer Nature Switzerland.
doi: 10.1007/978-3-032-16855-9_19
@InBook{mogue:mf60, pages = {445--463},
title = {Secure Set-Based State Estimation of Multi-sensor Switched Systems: An Impulsive-Switched Observer Approach},
publisher = {Springer Nature Switzerland},
year = {2026},
author = {Tagne Mogue, Ruth Line and Meslem, Nacim and Becis-Aubry, Yasmina and Courtial, Estelle and Ramdani, Nacim},
editor = {Rauh, Andreas and Finkbeiner, Bernd and Kr{\"o}ger, Paul},
address = {Cham},
isbn = {978-3-032-16855-9},
abstract = {This paper addresses the secure set-based state estimation for multi-sensor switched linear systems subject to distinguishable false-data injection and denial-of-service attacks. An intrusion detection algorithm based on interval analysis and impulsive-switched observer design is introduced to identify attacked sensors and provide secure set-based estimation. The stability guarantees for the interval impulsive-switched observer are derived using {\$}{\$}{\backslash}mathcal {\{}L{\}}{\_}1{\$}{\$}L1stability theory for hybrid systems. The proposed methodology is supported by theoretical analysis and illustrated through an application example.},
booktitle = {Design and Verification of Cyber-Physical Systems: From Theory to Applications: Essays Dedicated to Martin Fr{\"a}nzle on the Occasion of His 60th Birthday},
doi = {10.1007/978-3-032-16855-9_19},
url = {https://doi.org/10.1007/978-3-032-16855-9_19},
}
C. Neurohr, L. Westhofen, T. Koopmann, E. Möhlmann, E. Böde, and A. Hahn, "On Scenario Formalisms for Automated Driving" , Rauh, A., Finkbeiner, B., and Kröger, P. Eds., Cham: Springer Nature Switzerland.
doi: 10.1007/978-3-032-16855-9_17
@InBook{neurohr:mf60, pages = {403--425},
title = {On Scenario Formalisms for Automated Driving},
publisher = {Springer Nature Switzerland},
year = {2026},
author = {Neurohr, Christian and Westhofen, Lukas and Koopmann, Tjark and M{\"o}hlmann, Eike and B{\"o}de, Eckard and Hahn, Axel},
editor = {Rauh, Andreas and Finkbeiner, Bernd and Kr{\"o}ger, Paul},
address = {Cham},
isbn = {978-3-032-16855-9},
abstract = {The concept of scenario and its many qualifications -- specifically logical and abstract scenarios -- have emerged as a foundational element in safeguarding automated driving systems. However, the original linguistic definitions of the different scenario qualifications were often applied ambiguously, leading to a divergence between scenario description languages proposed or standardized in practice and their terminological foundation. This resulted in confusion about the unique features as well as strengths and weaknesses of logical and abstract scenarios. To alleviate this, we give clear linguistic definitions for the scenario qualifications concrete, logical, and abstract scenario and propose generic, unifying formalisms using curves, mappings to sets of curves, and temporal logics, respectively. We demonstrate that these formalisms allow pinpointing strengths and weaknesses precisely by comparing expressiveness, specification complexity, sampling, and monitoring of logical and abstract scenarios. Our work hence enables the practitioner to comprehend the different scenario qualifications and identify a suitable formalism.},
booktitle = {Design and Verification of Cyber-Physical Systems: From Theory to Applications: Essays Dedicated to Martin Fr{\"a}nzle on the Occasion of His 60th Birthday},
doi = {10.1007/978-3-032-16855-9_17},
url = {https://doi.org/10.1007/978-3-032-16855-9_17},
}
E. Olderog and M. Swaminathan, "Robust Structural Transformations for Real-Time Systems" , Rauh, A., Finkbeiner, B., and Kröger, P. Eds., Cham: Springer Nature Switzerland.
doi: 10.1007/978-3-032-16855-9_1
@InBook{olderog:mf60, pages = {3--23},
title = {Robust Structural Transformations for Real-Time Systems},
publisher = {Springer Nature Switzerland},
year = {2026},
author = {Olderog, Ernst-R{\"u}diger and Swaminathan, Mani},
editor = {Rauh, Andreas and Finkbeiner, Bernd and Kr{\"o}ger, Paul},
address = {Cham},
isbn = {978-3-032-16855-9},
abstract = {In previous work, we introduced structural transformations for data-enriched real-time systems modelled by extended timed automata, aiming at a simplification of the verification of such systems. There we assumed perfectly synchronous clocks proceeding at the same rate across the systems. In this paper, we permit that clocks may be subject to (sufficiently small) bounded drifts. We consider the transformations of layering and of flattening, and show that under reasonable conditions these transformations are robust against such bounded drifts in clocks. We illustrate this using a parameterized version of Fischer's real-time protocol for mutual exclusion.},
booktitle = {Design and Verification of Cyber-Physical Systems: From Theory to Applications: Essays Dedicated to Martin Fr{\"a}nzle on the Occasion of His 60th Birthday},
doi = {10.1007/978-3-032-16855-9_1},
url = {https://doi.org/10.1007/978-3-032-16855-9_1},
}
J. Peleska, F. Brüning, A. E. Haxthausen, and W. Huang, "A Scenario Specification Language for Testing Complex Cyber-Physical Systems" , Rauh, A., Finkbeiner, B., and Kröger, P. Eds., Cham: Springer Nature Switzerland.
doi: 10.1007/978-3-032-16855-9_15
@InBook{peleska:mf60, pages = {348--377},
title = {A Scenario Specification Language for Testing Complex Cyber-Physical Systems},
publisher = {Springer Nature Switzerland},
year = {2026},
author = {Peleska, Jan and Br{\"u}ning, Felix and Haxthausen, Anne E. and Huang, Wen-ling},
editor = {Rauh, Andreas and Finkbeiner, Bernd and Kr{\"o}ger, Paul},
address = {Cham},
isbn = {978-3-032-16855-9},
abstract = {According to the current state of practice, highly complex systems are no longer specified by comprehensive, monolithic models. Instead, relevant behaviours are represented separately as parametrised scenarios, and the overall system behaviour is derived from the resulting scenario library. This library concept has originally been advocated for the purpose of creating test references for autonomous road vehicles. Currently, scenario libraries are the preferred approach to specify the expected behaviour of any type of highly complex systems, both as an input to the design phase and as a collection of reference models for testing campaigns. In this paper, we introduce the novel scenario specification language SCSL and explain its syntax and semantics. In contrast to existing scenario modelling alternatives that are tightly bound to a specific application domain, the SCSL is domain-independent, but domain-specific support can be added in the form of re-usable specification libraries.},
booktitle = {Design and Verification of Cyber-Physical Systems: From Theory to Applications: Essays Dedicated to Martin Fr{\"a}nzle on the Occasion of His 60th Birthday},
doi = {10.1007/978-3-032-16855-9_15},
url = {https://doi.org/10.1007/978-3-032-16855-9_15},
}
C. Scholl, "A Review of Arithmetic Circuit Verification Using Symbolic Computer Algebra" , Rauh, A., Finkbeiner, B., and Kröger, P. Eds., Cham: Springer Nature Switzerland.
doi: 10.1007/978-3-032-16855-9_20
@InBook{scholl:mf60, pages = {464--503},
title = {A Review of Arithmetic Circuit Verification Using Symbolic Computer Algebra},
publisher = {Springer Nature Switzerland},
year = {2026},
author = {Scholl, Christoph},
editor = {Rauh, Andreas and Finkbeiner, Bernd and Kr{\"o}ger, Paul},
address = {Cham},
isbn = {978-3-032-16855-9},
abstract = {In recent years, the use of Symbolic Computer Algebra (SCA) has enabled a huge progress in the formal verification of arithmetic circuits. Several different approaches have been proposed showing great success especially for the verification of integer multipliers, but more recently also for the verification of integer dividers. The goal of this paper is to provide a comprehensive review of the current state of the art in arithmetic circuit verification using SCA, starting with a careful review of the underlying theory, through the identification of main challenges in arithmetic circuit verification, an overview of numerous non-trivial optimization methods, to an experimental evaluation of SCA-based verification.},
booktitle = {Design and Verification of Cyber-Physical Systems: From Theory to Applications: Essays Dedicated to Martin Fr{\"a}nzle on the Occasion of His 60th Birthday},
doi = {10.1007/978-3-032-16855-9_20},
url = {https://doi.org/10.1007/978-3-032-16855-9_20},
}
M. Schwammberger, A. Rakow, L. Putze, and A. Bairy, "Explain it for Safety: Explanations for Risk Mitigation" , Rauh, A., Finkbeiner, B., and Kröger, P. Eds., Cham: Springer Nature Switzerland.
doi: 10.1007/978-3-032-16855-9_16
@InBook{schwammberger:mf60, pages = {378--402},
title = {Explain it for Safety: Explanations for Risk Mitigation},
publisher = {Springer Nature Switzerland},
year = {2026},
author = {Schwammberger, Maike and Rakow, Astrid and Putze, Lina and Bairy, Akhila},
editor = {Rauh, Andreas and Finkbeiner, Bernd and Kr{\"o}ger, Paul},
address = {Cham},
isbn = {978-3-032-16855-9},
abstract = {Autonomous vehicles (AVs) must realise their mission goals while they navigate through hazards prioritising safety. These conflict situations often involve significant risks for all traffic participants. We postulate a key benefit of incorporating explanations in such high-risk scenarios: when delivered to the right recipient at the right time, an explanation can reduce risks in conflict situations. This paper advocates for explanations that not only enhance understanding of conflicts but actively contribute to their resolution. We illustrate our case with examples of high-risk conflict scenarios and derive essential design processes and requirements for risk-mitigating explanations.},
booktitle = {Design and Verification of Cyber-Physical Systems: From Theory to Applications: Essays Dedicated to Martin Fr{\"a}nzle on the Occasion of His 60th Birthday},
doi = {10.1007/978-3-032-16855-9_16},
url = {https://doi.org/10.1007/978-3-032-16855-9_16},
}
V. Sofronie-Stokkermans and P. Marohn, "On Verification and Constraint Generation for Families of Similar Hybrid Automata" , Rauh, A., Finkbeiner, B., and Kröger, P. Eds., Cham: Springer Nature Switzerland.
doi: 10.1007/978-3-032-16855-9_6
@InBook{sofronie:mf60, pages = {126--149},
title = {On Verification and Constraint Generation for Families of Similar Hybrid Automata},
publisher = {Springer Nature Switzerland},
year = {2026},
author = {Sofronie-Stokkermans, Viorica and Marohn, Philipp},
editor = {Rauh, Andreas and Finkbeiner, Bernd and Kr{\"o}ger, Paul},
address = {Cham},
isbn = {978-3-032-16855-9},
abstract = {In this paper we give an overview of results on the analysis of parametric linear hybrid automata, and of systems of similar linear hybrid automata: We consider, for instance, systems with a parametric (i.e. not explicitly specified) number of similar components, which can be connected to other systems, and in which the properties of some function symbols might be underspecified, and global safety properties which can be expressed by universally quantified first-order formulae, using quantification over variables ranging over the component systems.},
booktitle = {Design and Verification of Cyber-Physical Systems: From Theory to Applications: Essays Dedicated to Martin Fr{\"a}nzle on the Occasion of His 60th Birthday},
doi = {10.1007/978-3-032-16855-9_6},
url = {https://doi.org/10.1007/978-3-032-16855-9_6},
}
L. Weingarten, K. Datta, S. Ahmadi-Pour, A. Kole, and R. Drechsler, "Ensuring Correctness Efficiently for RISC-V Processors with Customised Multiplier Designs" , Rauh, A., Finkbeiner, B., and Kröger, P. Eds., Cham: Springer Nature Switzerland.
doi: 10.1007/978-3-032-16855-9_21
@InBook{weingarten:mf60, pages = {504--519},
title = {Ensuring Correctness Efficiently for RISC-V Processors with Customised Multiplier Designs},
publisher = {Springer Nature Switzerland},
year = {2026},
author = {Weingarten, Lennart and Datta, Kamalika and Ahmadi-Pour, Sallar and Kole, Abhoy and Drechsler, Rolf},
editor = {Rauh, Andreas and Finkbeiner, Bernd and Kr{\"o}ger, Paul},
address = {Cham},
isbn = {978-3-032-16855-9},
abstract = {Polynomial Formal Verification (PFV) is considered as a specific class of formal verification methodology that targets verification within space and time limits. Several works have already focused on PFV of arithmetic circuits and processors. PFV of processors, as reported in recent work, only considers the base instruction set, but no multiplier units were taken into account. In this paper, we modify the processor design by adding custom multiplier with a range of verifiable multiplier designs. We exploit Symbolic Computer Algebra (SCA) for performing verification of the multipliers and use Binary Decision Diagrams (BDDs) for the other instructions. Although multiplier verification is itself a challenging task, we particularly show that with some constraints on the structure of the multiplier, the verification process can be achieved in polynomial time. We extend the processor design as reported in the earlier work by including custom multipliers that can be verified within reasonable time. We also design the necessary software tools required to automate the entire verification process. The MicroRV32 RISC-V processor is used as a case study to evaluate the proposed verification methodology. Experimental results show that formal verification can indeed be performed within polynomial bounds for some of the processor units.},
booktitle = {Design and Verification of Cyber-Physical Systems: From Theory to Applications: Essays Dedicated to Martin Fr{\"a}nzle on the Occasion of His 60th Birthday},
doi = {10.1007/978-3-032-16855-9_21},
url = {https://doi.org/10.1007/978-3-032-16855-9_21},
}
K. G. Larsen and M. Zimmermann, "You May Delay, but Time Will Not: Timed Games Under Delayed Control" , Rauh, A., Finkbeiner, B., and Kröger, P. Eds., Cham: Springer Nature Switzerland.
doi: 10.1007/978-3-032-16855-9_2
@InBook{zimmermann:mf60, pages = {24--47},
title = {You May Delay, but Time Will Not: Timed Games Under Delayed Control},
publisher = {Springer Nature Switzerland},
year = {2026},
author = {Larsen, Kim G. and Zimmermann, Martin},
editor = {Rauh, Andreas and Finkbeiner, Bernd and Kr{\"o}ger, Paul},
address = {Cham},
isbn = {978-3-032-16855-9},
abstract = {Inspired by Martin Fr{\"a}nzle's persistent and influential work on capturing and handling delay inherent to cyber-physical systems in the formal verification of such systems, we study timed games where controllable actions do not take effect immediately, but only after some delay, i.e., they are scheduled for later execution.},
booktitle = {Design and Verification of Cyber-Physical Systems: From Theory to Applications: Essays Dedicated to Martin Fr{\"a}nzle on the Occasion of His 60th Birthday},
doi = {10.1007/978-3-032-16855-9_2},
url = {https://doi.org/10.1007/978-3-032-16855-9_2},
}
S. Khajei and J. W. Rieger, "A Review of Cyber-Physical Systems in Driving: Assisting Older People" , Rauh, A., Finkbeiner, B., and Kröger, P. Eds., Cham: Springer Nature Switzerland.
doi: 10.1007/978-3-032-16855-9_24
@InBook{khajei:mf60, pages = {564--577},
title = {A Review of Cyber-Physical Systems in Driving: Assisting Older People},
publisher = {Springer Nature Switzerland},
year = {2026},
author = {Khajei, Sina and Rieger, Jochem W.},
editor = {Rauh, Andreas and Finkbeiner, Bernd and Kr{\"o}ger, Paul},
address = {Cham},
isbn = {978-3-032-16855-9},
__markedentry = {[pkroeger:]},
abstract = {Driving is essential for the mobility and independence of older people. However, aging is usually associated with various types of cognitive decline, as well as physical and mental complications. European senior drivers have the second highest mortality rate in road traffic accidents compared to other age groups. Therefore, it is necessary to understand the physical/cognitive problems of senior drivers that increase their vulnerability and to find efficient ways to deal with them. In this review, we first provide evidence for increased seniors' driving risks. We then compare the cognitive and physical abilities of older and younger drivers. In the next section, mobility-related driving problems are discussed. Existing solutions are summarized, and systems for hazard detection and driver assistance are reviewed. The final sections examine the progress towards partially/fully autonomous vehicles and their potential utilities and risks.},
booktitle = {Design and Verification of Cyber-Physical Systems: From Theory to Applications: Essays Dedicated to Martin Fr{\"a}nzle on the Occasion of His 60th Birthday},
doi = {10.1007/978-3-032-16855-9_24},
url = {https://doi.org/10.1007/978-3-032-16855-9_24},
}
M. Schmidt, S. Plambeck, and G. Fey, "Learnability of Models for Cyber-Physical Systems --- A Review" , Rauh, A., Finkbeiner, B., and Kröger, P. Eds., Cham: Springer Nature Switzerland.
doi: 10.1007/978-3-032-16855-9_23
@InBook{schmidt:mf60, pages = {543--563},
title = {Learnability of Models for Cyber-Physical Systems --- A Review},
publisher = {Springer Nature Switzerland},
year = {2026},
author = {Schmidt, Maximilian and Plambeck, Swantje and Fey, Goerschwin},
editor = {Rauh, Andreas and Finkbeiner, Bernd and Kr{\"o}ger, Paul},
address = {Cham},
isbn = {978-3-032-16855-9},
__markedentry = {[pkroeger:]},
abstract = {The complexity of Cyber-Physical Systems (CPS) emerges from a tight integration of numerous digital and physical components. Recent powerful machine learning algorithms are increasingly applied to learn models of CPS from data. However, theoretical limitations of such a pragmatic approach are often left aside.},
booktitle = {Design and Verification of Cyber-Physical Systems: From Theory to Applications: Essays Dedicated to Martin Fr{\"a}nzle on the Occasion of His 60th Birthday},
doi = {10.1007/978-3-032-16855-9_23},
url = {https://doi.org/10.1007/978-3-032-16855-9_23},
}
