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.

翻译：线性系统的控制设计工具通常涉及极点配置与李雅普诺夫函数计算，这些方法对确保系统稳定性至关重要。然而随着控制设计要求的提高，设计者还需满足安全或时序逻辑规范等其他约束，而朴素的控制设计可能无法满足此类规范。控制设计者可运用模型检测作为安全校验工具，在发生安全违例时获取反例。尽管当前已开发出多种可扩展的线性动力系统安全验证技术，但这些工具本质上仅作为系统安全性评估的判定程序，通过生成反例作为安全违例的实证依据。然而这些模型检测方法并未针对发现边界案例或复用验证构件以适配次优安全规范进行设计。本文提出一种技术，用于完整表征线性系统安全违例的反例。该技术利用给定时序逻辑公式安全验证过程中计算的可达集执行约束传播，并通过二叉决策图（BDD）表征所有反例模式。我们引入动态判定同构节点的方法，从而获得规模显著简化的决策图。基于多个基准测试的全面实验评估表明，该约简技术可将决策图节点数减少至多67%，宽度缩减至多75%。