Counterexample-Preserving Reduction for Symbolic Model Checking
المؤلفون المشاركون
Wang, Ji
Mao, Xiaoguang
Fu, Xianjin
Dong, Wei
Wang, Rui
Liu, Wanwei
المصدر
Journal of Applied Mathematics
العدد
المجلد 2014، العدد 2014 (31 ديسمبر/كانون الأول 2014)، ص ص. 1-13، 13ص.
الناشر
Hindawi Publishing Corporation
تاريخ النشر
2014-05-14
دولة النشر
مصر
عدد الصفحات
13
التخصصات الرئيسية
الملخص EN
The cost of LTL model checking is highly sensitive to the length of the formula under verification.
We observe that, under some specific conditions, the input LTL formula can be reduced to an easier-to-handle one before model checking.
In such reduction, these two formulae need not to be logically equivalent, but they share the same counterexample set w.r.t the model.
In the case that the model is symbolically represented, the condition enabling such reduction can be detected with a lightweight effort (e.g., with SAT-solving).
In this paper, we tentatively name such technique “counterexample-preserving reduction” (CePRe, for short), and the proposed technique is evaluated by conducting comparative experiments of BDD-based model checking, bounded model checking, and property directed reachability-(IC3) based model checking.
نمط استشهاد جمعية علماء النفس الأمريكية (APA)
Liu, Wanwei& Wang, Rui& Fu, Xianjin& Wang, Ji& Dong, Wei& Mao, Xiaoguang. 2014. Counterexample-Preserving Reduction for Symbolic Model Checking. Journal of Applied Mathematics،Vol. 2014, no. 2014, pp.1-13.
https://search.emarefa.net/detail/BIM-491705
نمط استشهاد الجمعية الأمريكية للغات الحديثة (MLA)
Liu, Wanwei…[et al.]. Counterexample-Preserving Reduction for Symbolic Model Checking. Journal of Applied Mathematics No. 2014 (2014), pp.1-13.
https://search.emarefa.net/detail/BIM-491705
نمط استشهاد الجمعية الطبية الأمريكية (AMA)
Liu, Wanwei& Wang, Rui& Fu, Xianjin& Wang, Ji& Dong, Wei& Mao, Xiaoguang. Counterexample-Preserving Reduction for Symbolic Model Checking. Journal of Applied Mathematics. 2014. Vol. 2014, no. 2014, pp.1-13.
https://search.emarefa.net/detail/BIM-491705
نوع البيانات
مقالات
لغة النص
الإنجليزية
الملاحظات
Includes bibliographical references
رقم السجل
BIM-491705
قاعدة معامل التأثير والاستشهادات المرجعية العربي "ارسيف Arcif"
أضخم قاعدة بيانات عربية للاستشهادات المرجعية للمجلات العلمية المحكمة الصادرة في العالم العربي
تقوم هذه الخدمة بالتحقق من التشابه أو الانتحال في الأبحاث والمقالات العلمية والأطروحات الجامعية والكتب والأبحاث باللغة العربية، وتحديد درجة التشابه أو أصالة الأعمال البحثية وحماية ملكيتها الفكرية. تعرف اكثر