BDD for Complete Characterization of a Safety Violation in Linear Systems with Inputs
The control design tools for linear systems typically involves pole placement and computing Lyapunov functions which are useful for ensuring stability. But given higher requirements on control design, a designer is expected to satisfy other specification such as safety or temporal logic specification as well, and a naive control design might not satisfy such specification. A control designer can employ model checking as a tool for checking safety and obtain a counterexample in case of a safety violation. While several scalable techniques for verification have been developed for safety verification of linear dynamical systems, such tools merely act as decision procedures to evaluate system safety and, consequently, yield a counterexample as an evidence to safety violation. However these model checking methods are not geared towards discovering corner cases or re-using verification artifacts for another sub-optimal safety specification. In this paper, we describe a technique for obtaining complete characterization of counterexamples for a safety violation in linear systems. The proposed technique uses the reachable set computed during safety verification for a given temporal logic formula, performs constraint propagation, and represents all modalities of counterexamples using a binary decision diagram (BDD). We introduce an approach to dynamically determine isomorphic nodes for obtaining a considerably reduced (in size) decision diagram. A thorough experimental evaluation on various benchmarks exhibits that the reduction technique achieves up to $67\%$ reduction in the number of nodes and $75\%$ reduction in the width of the decision diagram.
Code (0)
등록된 구현이 없습니다.
Methods 이 논문이 사용한 방법론
Similar Papers 제목 키워드 기반
Characterization of the Dynamical Properties of Safety Filters for Linear Planar Systems
This paper studies the dynamical properties of closed-loop systems obtained from control barrier function-based safety filters. We provide a sufficient and necessary condition for the existence of undesirable equilibria …
Sample-and-Hold Safety with Control Barrier Functions
A common assumption on the deployment of safeguarding controllers on the digital platform is that high sampling frequency translates to a small violation of safety. This paper investigates and formalizes this assumption …
On asymptotic characterization of destabilizing switching signals for switched linear systems
This paper deals with classes of (de)stabilizing switching signals for switched systems. Most of the available conditions for stability of switched systems are sufficient in nature, and consequently, their violation does…
On the Completeness and Ordering of Path-Complete Barrier Functions
This paper is concerned with path-complete barrier functions which offer a graph-based methodology for verifying safety properties in switched systems. The path-complete framework leverages algebraic (barrier functions) …
Risk-Aware Safe Reinforcement Learning for Control of Stochastic Linear Systems
This paper presents a risk-aware safe reinforcement learning (RL) control design for stochastic discrete-time linear systems. Rather than using a safety certifier to myopically intervene with the RL controller, a risk-in…
Reinforcement Learning (RL)Safe Reinforcement Learning