دانلود ترجمه مقاله انتزاع و تقریب در منطق و مدل های زمانی فازی – اسپرینگر 2014

انتزاع و تقریب در منطق و مدل های زمانی فازی

Abstraction and approximation in fuzzy temporal logics and models

چکیده

1- مقدمه

2- سابقه

2-1- چک کردن مدل

2-2- منطق موجهات

2-3- تعمیم های منطق زمانی

2-4- منطق فازی

2-5- اتوماتای متناهی غیر قطعی گذار فازی

3- مدل کریپکه فازی

4- CTL* فازی

5- قابلیت تقریب خواص زمانی FzCTL در FzKripke

6- تجرید کریپکه فازی و تقریب مدل تجریدی

6-1- هم ارزی شبیه سازی دو گانه

7- نمودار برنامه فازی

7-1- نمودار برنامه فازی ساده

7-2- هم ارزی بین نمودار برنامه فازی و کریپکه فازی

8- از FzPG تا FzKripke تجریدی و تقریبی مربوطه

8-1- فرمول تقریب پذیر – Δ نرمال

9- مطالعه موردی

10- نتیجه گیری و کارهای آتی

منابع

چکیده

اخیراً، با تعریف منطق زمانی فازی مناسب، خواص زمانی سیستم های دینامیکی در خلال فرآیند چک کردن یا وارسی مدل مشخص شده اند و در عین حال تعداد کمی از منطق های زمانی فازی همراه با مدل های توانمند مربوطه در مرحله طراحی سیستم توسعه یافته و به کار رفته اند، افزون بر این در صورت داشتن مدلی مناسب، این مدل از فقدان یک رویکرد توانمند چک کردن مدل نیز رنج می برد. برای مقابله با عدم قطعیت در پارادایم وارسی مدل، این مقاله یک مدل کریپکه فازی (FzKripke) را معرفی نموده و سپس یک رویکرد راستی آزمایی را با استفاده از منطق جدیدی به نام منطق درخت محاسبات فازی* (FzCTL*) ارائه می نماید. نه تنها با استفاده از مفاهیم شناخته شده ای مانند: تجرید و شبیه سازی دو گانه به مساله انفجار فضای حالت پرداخته شده بلکه یک روش تقریبی نیز به عنوان تکنیکی جدید برای مقابله با این مشکل ارائه گشته است. هم چنین نمودار برنامه فازی، که تعمیمی از نمودار برنامه و FzKripke محسوب می شود، در این مقاله با توجه به سطح بالاتر تجرید در ساخت مدل معرفی شده است. نهایتاً به منظور نشان دادن قابلیت مدل های پیشنهادی، مدلسازی و راستی آزمایی یک فلیپ فلاپ چند مقداری مورد مطالعه قرار گرفته است.

10- نتیجه گیری و کارهای آتی

در این مقاله، نه تنها ما به معرفی کریپکه فازی به عنوان یک مدل کریپکه چند مقداری بسط یافته پرداختیم بلکه یک منطق فازی زمانی (موسوم به FzCTL*) را نیز بر اساس FzKripke به منظور بیان خواص زمانی تعریف نمودیم. در واقع FzCTL* شامل برخی از اپراتورهایی می شود که به ندرت در دیگر منطق ها دیده می شوند. اصلاحاتی در معنای فرمول های ان برای اجتناب از نواقص منطق های دیگر مانند: ابهام صورت پذیرفته است. هم چنین FzKripke با راه حل های کلاسیک برای مشکل انفجار فضای حالت مطابقت دارد. به منظور کاهش فضای حالت، ما دو روش ارائه نمودیم؛ یکی تجرید با استفاده از شبیه سازی دو گانه بدون تاثیرگذاری بر مقدار گزاره های منطق، و دیگری یک تکنیک تقریب برای مدل و منطق گزاره. با اِعمال روش دوم، کاهش فضای حالت با میزان خطای کنترل شده برای مقادیر گزاره همراه است. ترکیبی از این دو روش نیز کاربردپذیر می باشد. در موضوع دیگر، یک مدل فشرده ای به نام FzPG تعریف گردید. مدل FzPG به راحتی قابل تبدیل به یک مدل کریپکه فازی نامتناهی است، و FzKripke نامتناهی نیز قابل تبدیل به یک FzKripke متناهی تقریبی با استفاده از تکنیک های تقریب و تجرید می باشد. هم چنین FzPG را می توان تحت شرایط خاصی تقریب زد.

Abstract

Recently, by defining suitable fuzzy temporal logics, temporal properties of dynamic systems are specified during model checking process, yet a few numbers of fuzzy temporal logics along with capable corresponding models are developed and used in system design phase, moreover in case of having a suitable model, it suffers from the lack of a capable model checking approach. Having to deal with uncertainty in model checking paradigm, this paper introduces a fuzzy Kripke model (FzKripke) and then provides a verification approach using a novel logic called Fuzzy Computation Tree Logic∗ (FzCTL∗). Not only state space explosion is handled using well-known concepts like abstraction and bisimulation, but an approximation method is also devised as a novel technique to deal with this problem. Fuzzy program graph, a generalization of program graph and FzKripke, is also introduced in this paper in consideration of higher level abstraction in model construction. Eventually modeling, and verification of a multi-valued flip-flop is studied in order to demonstrate capabilities of the proposed models.

10- Conclusion and future work

In this paper, not only we introduced Fuzzy Kripke as an extended multi-valued Kripke model but we also defined a temporal fuzzy logic (called FzCTL∗) based on FzKripke in order to express temporal properties. FzCTL* include some operators that are rarely seen in other logics. Some modifications are carried out in the meaning of its formulas to avoid shortages in other logics like ambiguity. The FzKripke complies with classic solutions for the problem of state space explosion. In order to reduce state space, we present two methods; first one is abstraction using bisimulation without affecting the value of logic propositions, and the second one is an approximation technique for both model and logic propositions. By applying the latter method, state space reduction comes with a controlled error rate for propositions values. A combination of these two methods is also applicable. In another issue, a compact model called FzPG was defined. FzPG is easily convertible to an infinite fuzzy Kripke model, and the infinite FzKripke is also convertible to an approximated finite one using approximation and abstraction techniques together. The FzPG can also be approximated under an especial circumstance.

تصویری از مقاله ترجمه و تایپ شده در نرم افزار ورد

انتزاع و تقریب در منطق و مدل های زمانی فازی

Abstraction and approximation in fuzzy temporal logics and models