Counterexample Guided Abstraction Refinement for Stability Analysis

被引:15
|
作者
Prabhakar, Pavithra [1 ]
Soto, Miriam Garcia [2 ,3 ]
机构
[1] Kansas State Univ, Manhattan, KS 66506 USA
[2] IMDEA Software Inst, Madrid, Spain
[3] Univ Politecn Madrid, Madrid, Spain
来源
COMPUTER AIDED VERIFICATION, (CAV 2016), PT I | 2016年 / 9779卷
关键词
SYSTEMS;
D O I
10.1007/978-3-319-41528-4_27
中图分类号
TP31 [计算机软件];
学科分类号
081202 ; 0835 ;
摘要
In this paper, we present a counterexample guided abstraction refinement (CEGAR) algorithm for stability analysis of polyhedral hybrid systems. Our results build upon a quantitative predicate abstraction and model-checking algorithm for stability analysis, which returns a counterexample indicating a potential reason for instability. The main contributions of this paper include the validation of the counterexample and refinement of the abstraction based on the analysis of the counterexample. The counterexample returned by the quantitative predicate abstraction analysis is a cycle such that the product of the weights on its edges is greater than 1. Validation involves checking if there exists an infinite diverging execution which follows the cycle infinitely many times. Unlike in the case of CEGAR for safety, the validation problem is not a bounded model-checking problem. Using novel insights, we present a simple characterization for the existence of an infinite diverging execution in terms of the satisfaction of a first order logic formula which can be efficiently solved. Similarly, the refinement is more involved, since, there is a priori no bound on the number of predecessor computation steps that need to be performed to invalidate the abstract counterexample. We present strategies for refinement based on the insights from the validation step. We have implemented the validation and refinement algorithms and use the stability verification tool AVERIST in the back end for performing the abstraction and model-checking. We compare the Cegar algorithm with AVERIST and report experimental results demonstrating the benefits of counterexample guided refinement.
引用
收藏
页码:495 / 512
页数:18
相关论文
共 50 条
  • [1] Counterexample guided spotlight abstraction refinement
    Toben, Tobe
    FORMAL TECHNIQUES FOR NETWORKED AND DISTRIBUTED SYSTEMS - FORTE 2008, 2008, 5048 : 21 - 36
  • [2] Counterexample-guided abstraction refinement
    Clarke, E
    TIME-ICTL 2003: 10TH INTERNATIONAL SYMPOSIUM ON TEMPORAL REPRESENTATION AND REASONING AND FOURTH INTERNATIONAL CONFERENCE ON TEMPORAL LOGIC, PROCEEDINGS, 2003, : 7 - 8
  • [3] VCEGAR: Verilog counterexample guided abstraction refinement
    Jain, Himanshu
    Kroening, Daniel
    Sharygina, Natasha
    Clarke, Edmund
    TOOLS AND ALGORITHMS FOR THE CONSTRUCTION AND ANALYSIS OF SYSTEMS, PROCEEDINGS, 2007, 4424 : 583 - +
  • [4] Counterexample guided abstraction refinement is better under equational abstraction
    Enea, Constantin
    FIFTEENTH IEEE INTERNATIONAL CONFERENCE AND WORKSHOPS ON THE ENGINEERING OF COMPUTER-BASED SYSTEMS, PROCEEDINGS, 2008, : 126 - 135
  • [5] Counterexample-guided abstraction refinement for the analysis of graph transformation systems
    Koenig, Barbara
    Kozioura, Vitali
    TOOLS AND ALGORITHMS FOR THE CONSTRUCTION AND ANALYSIS OF SYSTEMS, PROCEEDINGS, 2006, 3920 : 197 - 211
  • [6] Effective Heuristics for Counterexample-Guided Abstraction Refinement
    He, Fei
    Song, Xiaoyu
    Gu, Ming
    Sun, Jiaguang
    GLSVLSI'07: PROCEEDINGS OF THE 2007 ACM GREAT LAKES SYMPOSIUM ON VLSI, 2007, : 393 - 398
  • [7] Counterexample Guided Abstraction Refinement Algorithm for Propositional Circumscription
    Janota, Mikolas
    Grigore, Radu
    Marques-Silva, Joao
    LOGICS IN ARTIFICIAL INTELLIGENCE, JELIA 2010, 2010, 6341 : 195 - 207
  • [8] A probabilistic learning approach for counterexample guided abstraction refinement
    He, Fei
    Song, Xiaoyu
    Gu, Ming
    Sun, Jiaguang
    AUTOMATED TECHNOLOGY FOR VERIFICATION AND ANALYSIS, PROCEEDINGS, 2006, 4218 : 39 - 50
  • [9] SAT-based counterexample guided abstraction refinement
    Clarke, EM
    MODEL CHECKING SOFTWARE, PROCEEDINGS, 2002, 2318 : 1 - 1
  • [10] Counterexample guided abstraction refinement via program execution
    Kroening, D
    Groce, A
    Clarke, E
    FORMAL METHODS AND SOFTWARE ENGINEERING, PROCEEDINGS, 2004, 3308 : 224 - 238