کد مقاله کد نشریه سال انتشار مقاله انگلیسی نسخه تمام متن
439366 690535 2006 22 صفحه PDF دانلود رایگان
عنوان انگلیسی مقاله ISI
Counterexample-guided predicate abstraction of hybrid systems
موضوعات مرتبط
مهندسی و علوم پایه مهندسی کامپیوتر نظریه محاسباتی و ریاضیات
پیش نمایش صفحه اول مقاله
Counterexample-guided predicate abstraction of hybrid systems
چکیده انگلیسی

Predicate abstraction has emerged to be a powerful technique for extracting finite-state models from infinite-state systems, and has been recently shown to enhance the effectiveness of the reachability computation techniques for hybrid systems. Given a hybrid system with linear dynamics and a set of linear predicates, the verifier performs an on-the-fly search of the finite discrete quotient whose states correspond to the truth assignments to the input predicates. The success of this approach depends on the choice of the predicates used for abstraction. In this paper, we focus on identifying these predicates automatically by analyzing spurious counterexamples generated by the search in the abstract state-space. We present the basic techniques for discovering new predicates that will rule out closely related spurious counterexamples, optimizations of these techniques, implementation of these in the verification tool, and case studies demonstrating the promise of the approach.

ناشر
Database: Elsevier - ScienceDirect (ساینس دایرکت)
Journal: Theoretical Computer Science - Volume 354, Issue 2, 28 March 2006, Pages 250-271