Related papers: Invariant, Viability and Discriminating Kernel Und…

Zonotopes are widely used for over-approximating forward reachable sets of uncertain linear systems for verification purposes. In this paper, we use zonotopes to achieve more scalable algorithms that under-approximate backward reachable…

This paper considers the problem of set-based state estimation for linear time-invariant (LTI) systems under time-varying sensor attacks. Provided that the LTI system is stable and observable via every single sensor and that at least one…

Affine systems reachability is the basis of many verification methods. With further computation, methods exist to reason about richer models with inputs, nonlinear differential equations, and hybrid dynamics. As such, the scalability of…

Backward reachability analysis is essential to synthesizing controllers that ensure the correctness of closed-loop systems. This paper is concerned with developing scalable algorithms that under-approximate the backward reachable sets, for…

Computing the viability kernel is key in providing guarantees of safety and proving existence of safety-preserving controllers for constrained dynamical systems. Current numerical techniques that approximate this construct suffer from a…

In real world applications, uncertain parameters are the rule rather than the exception. We present a reachability algorithm for linear systems with uncertain parameters and inputs using set propagation of polynomial zonotopes. In contrast…

This paper proposes methods for reachability analysis of nonlinear systems in both open loop and closed loop with advanced controllers. The methods combine hybrid zonotopes, a construct called a state-update set, functional decomposition,…

Artificial neural networks have recently been utilized in many feedback control systems and introduced new challenges regarding the safety of such systems. This paper considers the safe verification problem for a dynamical system with a…

We study the problem of computing robust controllable sets for discrete-time linear systems with additive uncertainty. We propose a tractable and scalable approach to inner- and outer-approximate robust controllable sets using constrained…

Hybrid zonotopes generalize constrained zonotopes by introducing additional binary variables and possess some unique properties that make them convenient to represent nonconvex sets. This paper presents novel hybrid zonotope-based methods…

We employ reachability analysis in designing dynamic quantization schemes for the remote state estimation of linear systems over a finite date rate communication channel. The quantization region is dynamically updated at each transmission…

We present a scalable set-valued safety-preserving controller for constrained continuous-time linear time-invariant (LTI) systems subject to additive, unknown but bounded disturbance or uncertainty. The approach relies upon a conservative…

Efficiently handling time-triggered and possibly nondeterministic switches for hybrid systems reachability is a challenging task. In this paper we present an approach based on conservative set-based enclosure of the dynamics that can handle…

This paper presents new methods for set-valued state estimation and active fault diagnosis of linear descriptor systems. The algorithms are based on constrained zonotopes, a generalization of zonotopes capable of describing strongly…

Inner-approximate reachability analysis involves calculating subsets of reachable sets, known as inner-approximations. This analysis is crucial in the fields of dynamic systems analysis and control theory as it provides a reliable…

Sampled-data (SD) systems, which are composed of both discrete- and continuous-time components, are arguably one of the most common classes of cyberphysical systems in practice; most modern controllers are implemented on digital platforms…

We introduce sparse polynomial zonotopes, a new set representation for formal verification of hybrid systems. Sparse polynomial zonotopes can represent non-convex sets and are generalizations of zonotopes, polytopes, and Taylor models.…

We study the verification problem for closed-loop dynamical systems with neural-network controllers (NNCS). This problem is commonly reduced to computing the set of reachable states. When considering dynamical systems and neural networks in…

This paper proposes a method for set-valued state estimation of nonlinear, discrete-time systems. This is achieved by combining graphs of functions representing system dynamics and measurements with the hybrid zonotope set representation…

Hybrid systems play a crucial role in modeling real-world applications where discrete and continuous dynamics interact, including autonomous vehicles, power systems, and traffic networks. Safety verification for these systems requires…