Bounded Model Checking of ETL Cooperating with Finite and Looping Automata Connectives
المؤلفون المشاركون
Mao, Xiaoguang
Wang, Rui
Liu, Wanwei
Li, Tun
Wang, Ji
المصدر
Journal of Applied Mathematics
العدد
المجلد 2013، العدد 2013 (31 ديسمبر/كانون الأول 2013)، ص ص. 1-12، 12ص.
الناشر
Hindawi Publishing Corporation
تاريخ النشر
2013-07-14
دولة النشر
مصر
عدد الصفحات
12
التخصصات الرئيسية
الملخص EN
As a complementary technique of the BDD-based approach, bounded model checking (BMC) has been successfully applied to LTL symbolic model checking.
However, the expressiveness of LTL is rather limited, and some important properties cannot be captured by such logic.
In this paper, we present a semantic BMC encoding approach to deal with the mixture of ETLf and ETLl.
Since such kind of temporal logic involves both finite and looping automata as connectives, all regular properties can be succinctly specified with it.
The presented algorithm is integrated into the model checker ENuSMV, and the approach is evaluated via conducting a series of imperial experiments.
نمط استشهاد جمعية علماء النفس الأمريكية (APA)
Wang, Rui& Liu, Wanwei& Li, Tun& Mao, Xiaoguang& Wang, Ji. 2013. Bounded Model Checking of ETL Cooperating with Finite and Looping Automata Connectives. Journal of Applied Mathematics،Vol. 2013, no. 2013, pp.1-12.
https://search.emarefa.net/detail/BIM-473487
نمط استشهاد الجمعية الأمريكية للغات الحديثة (MLA)
Wang, Rui…[et al.]. Bounded Model Checking of ETL Cooperating with Finite and Looping Automata Connectives. Journal of Applied Mathematics No. 2013 (2013), pp.1-12.
https://search.emarefa.net/detail/BIM-473487
نمط استشهاد الجمعية الطبية الأمريكية (AMA)
Wang, Rui& Liu, Wanwei& Li, Tun& Mao, Xiaoguang& Wang, Ji. Bounded Model Checking of ETL Cooperating with Finite and Looping Automata Connectives. Journal of Applied Mathematics. 2013. Vol. 2013, no. 2013, pp.1-12.
https://search.emarefa.net/detail/BIM-473487
نوع البيانات
مقالات
لغة النص
الإنجليزية
الملاحظات
Includes bibliographical references
رقم السجل
BIM-473487
قاعدة معامل التأثير والاستشهادات المرجعية العربي "ارسيف Arcif"
أضخم قاعدة بيانات عربية للاستشهادات المرجعية للمجلات العلمية المحكمة الصادرة في العالم العربي
تقوم هذه الخدمة بالتحقق من التشابه أو الانتحال في الأبحاث والمقالات العلمية والأطروحات الجامعية والكتب والأبحاث باللغة العربية، وتحديد درجة التشابه أو أصالة الأعمال البحثية وحماية ملكيتها الفكرية. تعرف اكثر