Reachability Analysis Using Constrained Polynomial Logical Zonotopes
In this paper, we propose reachability analysis using constrained polynomial logical zonotopes. We perform reachability analysis to compute the set of states that could be reached. To do this, we utilize a recently introduced set representation called polynomial logical zonotopes for performing computationally efficient and exact reachability analysis on logical systems. Notably, polynomial logical zonotopes address the "curse of dimensionality" when analyzing the reachability of logical systems since the set representation can represent $2^h$ binary vectors using $h$ generators. After finishing the reachability analysis, the formal verification involves verifying whether the intersection of the calculated reachable set and the unsafe set is empty or not. Polynomial logical zonotopes lack closure under intersections, prompting the formulation of constrained polynomial logical zonotopes, which preserve the computational efficiency and exactness of polynomial logical zonotopes for reachability analysis while enabling exact intersections. Additionally, an extensive empirical study is presented to demonstrate and validate the advantages of constrained polynomial logical zonotopes.
Code (1)
Tasks
Computational EfficiencyMethods 이 논문이 사용한 방법론
Similar Papers 제목 키워드 기반
Data-Driven Nonconvex Reachability Analysis using Exact Multiplication
This paper addresses a fundamental challenge in data-driven reachability analysis: accurately representing and propagating non-convex reachable sets. We propose a novel approach using constrained polynomial zonotopes to …
Hybrid Polynomial Zonotopes: A Set Representation for Reachability Analysis in Hybrid Nonaffine Systems
Reachability analysis for hybrid nonaffine systems remains computationally challenging, as existing set representations--including constrained, polynomial, and hybrid zonotopes--either lose tightness under high-order non…
Computational EfficiencyEllipsotopes: Combining Ellipsoids and Zonotopes for Reachability Analysis and Fault Detection
Ellipsoids are a common representation for reachability analysis, because they can be transformed efficiently under affine maps, and allow conservative approximation of Minkowski sums, which let one incorporate uncertain…
Fault DetectionEfficient Backward Reachability Using the Minkowski Difference of Constrained Zonotopes
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 …
Reachability Analysis for Linear Systems with Uncertain Parameters using Polynomial Zonotopes
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 zon…