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

با تركيب منطق‌هاي زماني و منطق فازي مي‌توان منطق‌هاي جديدي ايجاد و از آن در وارسي خودكار مدل‌هاي پوياي فازي استفاده نمود. تاكنون در چند مقاله مدل‌هاي كريپكه فازي FzKripke و گراف برنامه فازي FzPG به عنوان دو مدل زماني فازي تعريف و جهت وارسي خواص زماني روي اين مدل‌ها، منطق زماني FzCTL ارائه شده و بدون ارائه الگوريتم وارسي مدل، كاربردهايي از آنها در وارسي مدارات منطقي فازي مانند فليپ - فلاپ‌هاي فازي معرفي شده است. در اين مقاله جهت برخورد با مشكل انفجار فضاي حالت در مدل‌هاي زماني فازي، روشي نمادين ارائه شده كه به كمك آن، مدل‌ها در قالبي بسيار فشرده ذخيره و پردازش مي‌شوند. در اين مقاله كارايي الگوريتم‌هاي طراحي‌شده نيز مورد ارزيابي تحليلي و تجربي قرار مي‌گيرند. به عنوان مطالعه موردي، كارايي روش در وارسي و كشف مخاطره پوياي يك مدار فليپ - فلاپ D فازي، مورد بررسي قرار گرفته و زمان اجرا و حافظه مصرفي الگوريتم در شرايط مختلف مدل، ارائه شده است