وارسی نمادین گزارههای منطق زمانی فازی روی گراف برنامه فازی
الموضوعات : electrical and computer engineeringغلامرضا ستوده 1 , علی موقر رحیمآبادی 2
1 - دانشگاه آزاد اسلامي، واحد علوم تحقيقات
2 - دانشگاه صنعتي شريف
الکلمات المفتاحية: وارسی مدل مدل کریپکه منطق زمانی فازی گراف برنامه فازی وارسی نمادین مدل,
ملخص المقالة :
با ترکیب منطقهای زمانی و منطق فازی میتوان منطقهای جدیدی ایجاد و از آن در وارسی خودکار مدلهای پویای فازی استفاده نمود. تاکنون در چند مقاله مدلهای کریپکه فازی FzKripke و گراف برنامه فازی FzPG به عنوان دو مدل زمانی فازی تعریف و جهت وارسی خواص زمانی روی این مدلها، منطق زمانی FzCTL ارائه شده و بدون ارائه الگوریتم وارسی مدل، کاربردهایی از آنها در وارسی مدارات منطقی فازی مانند فلیپ- فلاپهای فازی معرفی شده است. در این مقاله جهت برخورد با مشکل انفجار فضای حالت در مدلهای زمانی فازی، روشی نمادین ارائه شده که به کمک آن، مدلها در قالبی بسیار فشرده ذخیره و پردازش میشوند. در این مقاله کارایی الگوریتمهای طراحیشده نیز مورد ارزیابی تحلیلی و تجربی قرار میگیرند. به عنوان مطالعه موردی، کارایی روش در وارسی و کشف مخاطره پویای یک مدار فلیپ- فلاپ D فازی، مورد بررسی قرار گرفته و زمان اجرا و حافظه مصرفی الگوریتم در شرایط مختلف مدل، ارائه شده است
