کد مقاله کد نشریه سال انتشار مقاله انگلیسی نسخه تمام متن
433375 1441679 2014 25 صفحه PDF دانلود رایگان
عنوان انگلیسی مقاله ISI
Symbolic counterexample generation for large discrete-time Markov chains
ترجمه فارسی عنوان
نسل متضاد نمادین برای زنجیره های مارکوف بزرگ زمان گسسته
کلمات کلیدی
موضوعات مرتبط
مهندسی و علوم پایه مهندسی کامپیوتر نظریه محاسباتی و ریاضیات
چکیده انگلیسی


• We present a general framework for generating counterexamples symbolically for large discrete-time Markov chains.
• We use SAT-solving techniques as well as symbolic graph algorithms.
• We provide a large comparison between explicit and symbolic approaches for counterexample generation.
• Our benchmarks show that we are able to generate counterexamples for systems with billions of states.

This paper presents several symbolic counterexample generation algorithms for discrete-time Markov chains (DTMCs) violating a PCTL formula. A counterexample is (a symbolic representation of) a sub-DTMC that is incrementally generated. The crux to this incremental approach is the symbolic generation of paths that belong to the counterexample. We consider two approaches. First, we extend bounded model checking and develop a simple heuristic to generate highly probable paths first. We then complement the SAT-based approach by a fully (multi-terminal) BDD-based technique. All symbolic approaches are implemented, and our experimental results show a substantially better scalability than existing explicit techniques. In particular, our BDD-based approach using a method called fragment search allows for counterexample generation for DTMCs with billions of states (up to 1015).

ناشر
Database: Elsevier - ScienceDirect (ساینس دایرکت)
Journal: Science of Computer Programming - Volume 91, Part A, 1 October 2014, Pages 90–114
نویسندگان
, , , , , , ,