Polynomial zonotopes are a non-convex set representation that have many applications, such as reachability analysis of hybrid systems, control in robotics, and verification of nonlinear systems. Such analysis methods often require intersection checking. The usual algorithm for intersection checking is to, first, overapproximate the polynomial zonotope by a zonotope and then, if the overapproximation is too large, split the set and recursively and repeat. Although the overapproximation error in this algorithm converges to the original polynomial zonotope, there are still two problems. First, the overapproximation error is not monotonically decreasing after each split. Second, more critically, the split polynomial zonotopes do not preserve the sparsity structure as the original polynomial zonotope, eliminating any memory and other efficiency benefits made possible by the sparse structure. In this paper, we propose a variation of polynomial zonotopes called denormalized polynomial zonotopes, where each factor variable does not need to be in the range [-1, 1]. We prove this slight modification eliminates the two above issues, while still guaranteeing that overapproximation error will converge to the exact polynomial zonotope. We demonstrate the efficiency improvements through numerical experiments, where in certain cases denormalized polynomial zonotope intersection checking is over 400x faster and uses 550x less memory.
We study control design methods to endow hybrid systems under disturbances with safety guarantees as an inverse-optimality problem. First, we provide sufficient conditions to guarantee inputto-state safety of a hybrid system with disturbance inputs only. Next, given a nominal feedback law, we show that a hybrid system, with inputs and disturbances, can be rendered input-to-state controlled safe under the existence of a control barrier function (CBF) using pointwise min-norm safeguarding feedback laws. Finally, we demonstrate that every CBF is a meaningful value function for a two-player zero-sum hybrid game in the context of safety, and that every pointwise min-norm safeguarding feedback law is optimal for such a game, even though its design is independent of any cost functional. The main results are illustrated in an example.
Hybrid games are a powerful framework for modelling interactions between cyber-physical systems (CPS). While their high level of nondeterminism allows the modelling of complex systems, it also makes many properties undecidable. This paper presents Hybrid Games with Triggers (HGT), an extension that reduces nondeterminism by embedding agents' rational decision-making as triggers conditions that, when met, prompt the agents to act. This approach leads to a time-abstract discrete game with a countable state space, where an agent has a winning strategy in the discrete game if and only if they do in the HGT. Our discretisation preserves both the continuous and discrete dynamics of the original hybrid game, providing a more structured, analysable model without sacrificing dynamic expressivity.
The increasing complexity of robotic and cyber-physical systems (CPS) has made specifying task plans with explicit timing requirements a significant challenge. Temporal logics such as Linear Temporal Logic (LTL) and Metric Interval Temporal Logic (MITL) are widely used for expressing temporally evolving tasks, but encoding recovery behaviors and interdependent objectives often leads to intractable synthesis and verification problems. Behavior Trees (BTs), originally developed in the gaming industry and now widely adopted in robotics, offer a graphical, modular, and dynamic alternative. Their flexibility supports reconfiguration without complete redesign, making them suitable for dynamic environments. Temporal Behavior Trees (TBTs) extend BTs by embedding Signal Temporal Logic (STL) formulas at leaf nodes, enabling quantitative semantics; however, they remain limited to offline monitoring and synthesis capabilities needed for adaptive control. To address this gap, we introduce BT2Automata, a framework that translates BTs into Timed Automata (TA), thereby bridging BTs' interpretability and modularity with the rigorous formal verification capabilities of temporal logic. While temporal logics excel at specifying temporally evolving behaviors but struggle with tractable synthesis, BTs provide dynamic adaptability but complicate safety analysis and control guarantees. By enabling falsification through UPPAAL, BT2Automata identifies inconsistencies, ensures language completeness under timing constraints, and supports monitoring of temporal properties. Furthermore, it enables both automaton-based and sampling-based control synthesis strategies that guarantee task satisfaction. This unified approach combines the intuitive specification advantages of BTs with the formal rigor of TA verification, advancing the development of adaptive, safe, and reliable control for CPS operating in safety-critical environments. This presentation is based on a HSCC 2025 paper [1].
Verifying the safety of latency-aware cyber-physical systems is both critical and challenging due to the interaction between continuous physical dynamics and discrete computational constraints. This paper introduces SOTERIA, a formal framework that integrates digital twins for ensuring safety in these systems. SOTERIA models both the physical dynamics and computational behavior, enabling integrated verification within a specific operating environment. This approach goes beyond conventional methods that either treat physical and computational aspects separately or rely on overly conservative worst-case analyses. By modeling hybrid dynamics alongside computational models and operating environments, SOTERIA verifies both functional and timing correctness. Leveraging established verification tools, SOTERIA determines whether end-to-end latencies meet formal specifications, bridging the gap between computational and physical requirements. We first introduce a simple example of a 1D adaptive cruise control system to illustrate its effectiveness. We then present findings from a case study using the F1Tenth racing car platform and the UPPAAL tool to demonstrate SOTERIA's effectiveness in realistic scenarios, enabling safety verification that was previously infeasible with conventional schedulability analyses. This work underscores the importance of an integrated verification approach for enhancing safety and reliability in autonomous systems.
This paper introduces a novel quantitative verification framework for analyzing the temporal behaviors of learning-enabled systems (LES). Our approach employs ProbStar Temporal Logic (ProbStarTL) to specify LES temporal behaviors alongside advanced reachability and verification algorithms. Unlike existing qualitative methods focusing primarily on reach-avoid properties, our framework enables quantitative analysis of temporal properties. ProbStarTL, distinct from Signal Temporal Logic, operates on sequences of timed probabilistic star reachable sets, known as ProbStar signals. It features a clear syntax and dual qualitative and quantitative semantics. Our framework includes depth-first search algorithms for generating ProbStar traces and novel verification algorithms that transform ProbStarTL specifications into a computable disjunctive normal form for analysis. Our verification algorithms allow for both exact and approximate analyses. The exact scheme guarantees sound and complete results with precise satisfaction probabilities, while the approximate scheme offers sound results with maximum and minimum satisfaction probabilities at a reduced computational cost. The new verification framework is implemented using StarV, and its effectiveness is demonstrated through case studies on a learningbased adaptive cruise control system and an advanced emergency braking system.
We study localization and control problems in which agent dynamics are described by difference or differential equations, while output measurements are collected at discrete times and given by finite-valued maps depending on possibly unknown landmark locations. Guided by the goal of understanding fundamental limitations imposed by such coarse measurements, we focus on characterizing indistinguishable states, i.e., agent-landmark pairs that produce identical observations under all control inputs. We show that indistinguishability relations can be checked automatically under mild assumptions and, being a special type of bisimulation, we develop an iterative algorithm for approximately computing them. We then introduce an analytical approach, rooted in observability theory of linear control systems, which iteratively computes a sequence of subspaces converging in finitely many steps to the indistinguishable subspace; a differential-geometric extension to nonlinear systems is also outlined.
Tight coupling between computation, communication, and control pervades the design and application of cyber-physical systems (CPSs). Due to the complexity of these systems, advanced design procedures that account for these tight interconnections are paramount to ensure the safe and reliable operation of control algorithms under computational constraints. This paper presents the Simulator for Hardware Architecture and Real-time Control (Sharc) to assist in the co-design of control algorithms and the computational hardware on which they are run. Sharc simulates the execution of a user-specified control algorithm on a given processor microarchitecture configuration, evaluating how computational constraints affect the dynamical properties of the closed-loop system. We illustrate the power of Sharc by examples of MPC applied to adaptive cruise control and the stabilization of an inverted pendulum. Sharc can be found at github.com/pwintz/sharc.
We present a counterexample-guided approach for synthesizing convex piecewise affine control Lyapunov functions, obtained as the maximum over a finite number of affine functions, for stabilizing switched linear systems. Our approach considers systems whose dynamics are defined by a set of affine ODEs over different regions of the state-space. The goal is to synthesize a control feedback function that uses state-based switching by assigning a dynamical mode to each state from the set of available dynamics. This is achieved by synthesizing a piecewise affine control Lyapunov function that guarantees that for each state variable, the appropriate choice of a control input can cause an instantaneous decrease in the value of the Lyapunov function. Since piecewise affine functions are not smooth, we use a non-smooth analytic characterization of piecewise affine Lyapunov functions. The key contribution of our approach is a counterexample driven algorithm that alternates between verification that a given convex PWA function is a control Lyapunov function or generating a counterexample point where the Lyapunov conditions fail, and synthesis from a finite set of counterexamples generated in the past. We demonstrate that the two steps can be performed using mixed integer linear programming problems (MILP) although no termination guarantees are possible. We show that the branch and cut approach used inside a MILP solver can be adapted to yield a termination guarantee. Although the resulting approach is computationally expensive, it has the advantage of not requiring a "demonstrator" or a pre-existing controller. We provide an empirical evaluation that explores the results of this approach over a set of numerical examples.
In recent years, many different methods for identifying hybrid automata from data have been proposed. However, most of these methods consider clean simulator data, and consequently do not perform well for noisy data measured from real systems. We address this shortcoming with a new approach for the identification of hybrid automata that is specifically designed to be robust to noise. In particular, we propose a new high-level strategy consisting of the following three steps: clustering based on the dynamics identified from a local dataset, state space partitioning using decision trees, and conversion of the decision tree to a hybrid automaton. In addition, we introduce several new concepts for the realization of the single steps. For example, we propose an automated regularization of the dynamic models used for clustering via rank adaptation, as well as a new variant of the Gini impurity index for decision tree learning, tailored toward hybrid systems where different dynamics can be active within the same state space region. As our experiments on 19 challenging benchmarks with different characteristics demonstrate, in addition to being robust to both process and measurement noise, our approach avoids the need for extensive hyper-parameter tuning and also performs well for clean data without noise. This presentation is based on a HSCC'25 paper [1].
We present the idea of successive control barrier functions for nonlinear (polynomial) control systems. Control Barrier Functions (CBFs) can be used to maintain safety properties for a system through the online modification of control inputs to ensure that the state remains inside a controlled invariant set that excludes a set of unsafe states. However, the synthesis of CBFs is quite difficult in practice, especially for nonlinear dynamical systems. Computationally inexpensive approaches employ relaxed control barrier conditions that result in relatively small control invariant sets. In turn, this can result in unnecessary modification of the nominal control input to keep the dynamics inside this set. In this paper, we propose the concept of "successive" CBFs. Rather than rely on a single CBF, our approach uses a hierarchy of functions wherein functions at one level of a hierarchy become active only if the functions at the previous levels have "failed". Using a well-known approach to finding barrier functions for polynomial dynamical systems using sum of squares optimization, we show how to adapt it to synthesize successive barrier functions. We also provide "transit time" guarantees to construct a "chattering-free" runtime enforcement scheme that avoids collisions with fixed obstacles. We demonstrate our approach on a set of interesting nonlinear benchmarks, while comparing it with state of the art approaches for synthesizing CBFs.
Safety-critical controllers of complex systems are hard to construct manually. Automated approaches such as controller synthesis or learning provide a tempting alternative but usually lack explainability. To this end, learning decision trees (DTs) have been prevalently used towards an interpretable model of the generated controllers. However, DTs do not exploit shared decision-making, a key concept exploited in binary decision diagrams (BDDs) to reduce their size and thus improve explainability. In this work, we introduce predicate decision diagrams (PDDs) that extend BDDs with predicates and thus unite the advantages of DTs and BDDs for controller representation. We establish a synthesis pipeline for efficient construction of PDDs from DTs representing controllers, exploiting reduction techniques for BDDs also for PDDs.
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.
We propose a novel, multi-layered planning approach for computing paths that satisfy both kinodynamic and spatiotemporal constraints. Our three-part framework first establishes potential sequences to meet spatial constraints, using them to calculate a geometric lead path. This path then guides an asymptotically optimal sampling-based kinodynamic planner, which minimizes an STL-robustness cost to jointly satisfy spatiotemporal and kinodynamic constraints. In our experiments, we test our method with a velocity-controlled Ackerman-car model and demonstrate significant efficiency gains compared to prior art. Additionally, our method is able to generate complex path maneuvers, such as crossovers, something that previous methods had not demonstrated.
We offer a compositional data-driven scheme for synthesizing controllers that ensure global asymptotic stability (GAS) across large-scale interconnected networks, characterized by unknown mathematical models. In light of each network's configuration composed of numerous subsystems with smaller dimensions, our proposed framework gathers data from each subsystem's trajectory, enabling the design of local controllers that ensure input-to-state stability (ISS) properties over subsystems, signified by ISS Lyapunov functions. To accomplish this, we require only a single input-state trajectory from each unknown subsystem up to a specified time horizon, fulfilling certain rank conditions. Subsequently, under small-gain compositional reasoning, we leverage ISS Lyapunov functions derived from data to offer a control Lyapunov function (CLF) for the interconnected network, ensuring GAS certificate over the network. We demonstrate that while the computational complexity for designing a CLF increases polynomially with the network dimension using sum-of-squares (SOS) optimization, our compositional data-driven approach significantly mitigates it to linear with respect to the number of subsystems. We showcase the efficacy of our data-driven approach over a set of benchmarks, involving physical networks with diverse interconnection topologies.
TRUST is an open-source software tool developed for data-driven controller synthesis of dynamical systems with unknown mathematical models, ensuring either stability or safety properties. By collecting only a single input-state trajectory from the unknown system and satisfying a rank condition that ensures the system is persistently excited according to the Willems et al.'s fundamental lemma, TRUST aims to design either control Lyapunov functions (CLF) or control barrier certificates (CBC), along with their corresponding stability or safety controllers. The tool implements sum-of-squares (SOS) optimization programs solely based on data to enforce stability or safety properties across four system classes: (i) continuous-time nonlinear polynomial systems, (ii) continuous-time linear systems, (iii) discrete-time nonlinear polynomial systems, and (iv) discrete-time linear systems. TRUST is a Python-based web application featuring an intuitive, reactive graphic user interface (GUI) built with web technologies. It can be accessed at https://trust.tgo.dev or installed locally, and supports both manual data entry and data file uploads. Leveraging the power of the Python backend and a JavaScript frontend, TRUST is designed to be highly user-friendly and accessible across desktop, laptop, tablet, and mobile devices. We apply TRUST to a set of physical benchmarks with unknown dynamics, ensuring either stability or safety properties across the four supported classes of models.
Synthesizing safety controllers for general nonlinear systems is a highly challenging task, particularly when the system models are unknown, and input constraints are present. While some recent efforts have explored data-driven safety controller design for nonlinear systems, these approaches are primarily limited to specific classes of nonlinear dynamics (e.g., polynomials) and are not applicable to general nonlinear systems. This paper develops a direct data-driven approach for discrete-time general nonlinear systems, facilitating the simultaneous learning of control barrier certificates (CBCs) and dynamic controllers to ensure safety properties under input constraints. Specifically, by leveraging the adding-one-integrator approach, we incorporate the controller's dynamics into the system dynamics to synthesize a virtual static-feedback controller for the augmented system, resulting in a dynamic safety controller for the actual dynamics. We collect input-state data from the augmented system during a finite-time experiment, referred to as a single trajectory. Using this data, we learn augmented CBCs and the corresponding virtual safety controllers, ensuring the safety of the actual system and adherence to input constraints over a finite time horizon. We demonstrate that our proposed conditions boil down to some data-dependent linear matrix inequalities (LMIs), which are easy to satisfy. We showcase the effectiveness of our data-driven approach through two case studies: one exhibiting significant nonlinearity and the other featuring high dimensionality.
Finding Lyapunov functions to certify the stability of control systems has been an important topic for certifying safety-critical systems. Most existing methods on finding Lyapunov functions require access to the dynamics of the system. Accurately describing the complete dynamics of a control system however remains highly challenging in practice. Latest trend of using learning-enabled control systems further reduces the transparency. Hence, a method for black-box systems would have much wider applications. Our work stems from the idea of sampling and exploiting Lipschitz continuity to approximate the unknown dynamics. Given Lipschitz constants, one can derive a non-statistical upper bounds on approximation errors; hence a strong certification on this approximation can certify the unknown dynamics. We significantly improve this idea by directly approximating the Lie derivative of Lyapunov functions instead of the dynamics. We propose a framework based on the learner-verifier architecture from Counterexample-Guided Inductive Synthesis (CEGIS). Our insight of combining regional verification conditions and counterexample-guided sampling enables a guided search for samples to prove stability region-by-region. Our CEGIS algorithm further ensures termination. Our numerical experiments suggest that it is possible to prove the stability of 2D and 3D systems with a few thousands of samples. In comparison with the existing black-box approach, our approach at the best case requires less than 0.01% of samples.
