وارسی نمادین گزاره‌های منطق زمانی فازی روی گراف برنامه فازی

با ترکیب منطق‌های زمانی و منطق فازی می‌توان منطق‌های جدیدی ایجاد و از آن در وارسی خودکار مدل‌های پویای فازی استفاده نمود. تاکنون در چند مقاله مدل‌های کریپکه فازی fzkripke و گراف برنامه فازی fzpg به عنوان دو مدل زمانی فازی تعریف و جهت وارسی خواص زمانی روی این مدل‌ها، منطق زمانی fzctl ارائه شده و بدون ارائه الگوریتم وارسی مدل، کاربردهایی از آنها در وارسی مدارات منطقی فازی مانند فلیپ فلاپ‌های فازی معرفی شده است. در این مقاله جهت برخورد با مشکل انفجار فضای حالت در مدل‌های زمانی فازی، روشی نمادین ارائه شده که به کمک آن، مدل‌ها در قالبی بسیار فشرده ذخیره و پردازش می‌شوند. در این مقاله کارایی الگوریتم‌های طراحی‌شده نیز مورد ارزیابی تحلیلی و تجربی قرار می‌گیرند. به عنوان مطالعه موردی، کارایی روش در وارسی و کشف مخاطره پویای یک مدار فلیپ فلاپ d فازی، مورد بررسی قرار گرفته و زمان اجرا و حافظه مصرفی الگوریتم در شرایط مختلف مدل، ارائه شده است