کد مقاله | کد نشریه | سال انتشار | مقاله انگلیسی | نسخه تمام متن |
---|---|---|---|---|
4943819 | 1437715 | 2017 | 42 صفحه PDF | دانلود رایگان |
عنوان انگلیسی مقاله ISI
Quantitative model checking of linear-time properties based on generalized possibility measures
ترجمه فارسی عنوان
مدل کمی بررسی خصوصیات خطی زمان بر اساس معیارهای احتمالی تعمیم یافته
دانلود مقاله + سفارش ترجمه
دانلود مقاله ISI انگلیسی
رایگان برای ایرانیان
کلمات کلیدی
چک کردن مدل، نظریه احتمالی، منطق زمانی منطقی، اتوماتیک محدود فازی، زبان منظم فازی ساختار کریپی امکان پذیر است
موضوعات مرتبط
مهندسی و علوم پایه
مهندسی کامپیوتر
هوش مصنوعی
چکیده انگلیسی
Model checking of linear-time properties based on possibility measures was studied in previous work (Li and Li (2013)). However, the linear-time properties considered in the previous work was qualitative and was based on Boolean logic, the linear-time properties containing possibility information (we call it fuzzy linear-time properties here, which is based on fuzzy logic) of system could not be represented and tackled using the previous methods. We shall study quantitative model checking of fuzzy linear-time properties based on generalized possibility measures in the paper. Both the model of the system, as well as the properties the system needs to adhere to, are described using possibility information to identify the uncertainty in the model/properties. The systems are modeled by generalized possibilistic Kripke structures (GPKS, in short), and the properties are described by fuzzy linear-time properties. Concretely, fuzzy linear-time properties about reachability, always reachability, constrain reachability, repeated reachability and persistence in GPKSs are introduced and studied. Fuzzy regular safety properties and fuzzy Ï-regular properties in GPKSs are introduced, the verification of fuzzy regular safety properties and fuzzy Ï-regular properties using fuzzy finite automata are thoroughly studied. It has been shown that the verification of fuzzy regular safety properties and fuzzy Ï-regular properties in a finite GPKS can be transformed into the verification of (always) reachability properties and repeated reachability (persistence) properties in the product GPKS introduced in this paper. Several examples are given to illustrate the methods presented in the paper.
ناشر
Database: Elsevier - ScienceDirect (ساینس دایرکت)
Journal: Fuzzy Sets and Systems - Volume 320, 1 August 2017, Pages 17-39
Journal: Fuzzy Sets and Systems - Volume 320, 1 August 2017, Pages 17-39
نویسندگان
Yongming Li,