مرکز منطقه ای اطلاع رسانی علوم و فناوری فصلنامه مهندسی برق و مهندسی کامپيوتر ايران 16823745 15 1 2017 6 21 Symbolic Verification of Temporal Fuzzy Logic Properties on Fuzzy Program Graph وارسی نمادین گزاره‌های منطق زمانی فازی روی گراف برنامه فازی 55 63 fa غلامرضا ستوده علی موقر رحیم‌آبادی 2017 7 18 We may investigate the correctness of dynamic fuzzy models by a combination of Modal Temporal Logics and Fuzzy Logic. So far Fuzzy-extended Kripke structure (FzKripke) and Fuzzy-extended Program Graph (FzPG) are introduced as two timed Fuzzy logic models. Meanwhile, a Fuzzy-extended Temporal Logic (FzCTL) is introduced. Although no verification technique is devised for verifying FzCTL properties of timed Fuzzy logic models, its applications in verification of Fuzzy Logic Circuits (i.e., Fuzzy Flip-Flops) are studied and elaborated. In this paper we introduce a symbolic approach to tackle the state space explosion problem in timed Fuzzy logic models with which models are simultaneously compressed and processed in the most compact representation possible yet. The applicability of this approach is also demonstrated through experiments on a case study concerning dynamic hazards in a Fuzzy D-Flip Flop. Performance measures like runtime and memory consumptions are also provided for different scenarios. با ترکیب منطق‌های زمانی و منطق فازی می‌توان منطق‌های جدیدی ایجاد و از آن در وارسی خودکار مدل‌های پویای فازی استفاده نمود. تاکنون در چند مقاله مدل‌های کریپکه فازی FzKripke و گراف برنامه فازی FzPG به عنوان دو مدل زمانی فازی تعریف و جهت وارسی خواص زمانی روی این مدل‌ها، منطق زمانی FzCTL ارائه شده و بدون ارائه الگوریتم وارسی مدل، کاربردهایی از آنها در وارسی مدارات منطقی فازی مانند فلیپ- فلاپ‌های فازی معرفی شده است. در این مقاله جهت برخورد با مشکل انفجار فضای حالت در مدل‌های زمانی فازی، روشی نمادین ارائه شده که به کمک آن، مدل‌ها در قالبی بسیار فشرده ذخیره و پردازش می‌شوند. در این مقاله کارایی الگوریتم‌های طراحی‌شده نیز مورد ارزیابی تحلیلی و تجربی قرار می‌گیرند. به عنوان مطالعه موردی، کارایی روش در وارسی و کشف مخاطره پویای یک مدار فلیپ- فلاپ D فازی، مورد بررسی قرار گرفته و زمان اجرا و حافظه مصرفی الگوریتم در شرایط مختلف مدل، ارائه شده است http://ijece.org/ar/Article/Download/28237