Generating Longest Counterexample: On The Cross-Roads Of Mixed Integer Linear Programming And Smt
2020 AMERICAN CONTROL CONFERENCE (ACC)(2020)
摘要
We present a technique for obtaining the longest counterexample - the execution that stays in the unsafe set for the longest (not necessarily contiguous) time, for a safety specification of linear hybrid systems. Given that hybrid systems are infinite state systems, the number of counterexamples for safety violations are potentially infinite. Therefore, searching for the right counterexample is very challenging. We employ two frameworks for solving this problem: first is an Mixed Integer Linear Program (MILP) formulation and second is to encode counterexamples using Satisfiability Module Theory (SMT) solvers. We evaluate these frameworks on several linear hybrid systems with up to 30 dimensions.
更多查看译文
关键词
SMT,linear hybrid systems,mixed integer linear programming,unsafe set,safety specification,infinite state systems,satisfiability module theory solvers,MILP
AI 理解论文
溯源树
样例
生成溯源树,研究论文发展脉络