تجرید و تقریب در منطق و مدل های زمانی فازی
چکیده
اخیراً، با تعریف منطق زمانی فازی مناسب، خواص زمانی سیستم های دینامیکی در خلال فرآیند چک کردن یا وارسی مدل مشخص شده اند و در عین حال تعداد کمی از منطق های زمانی فازی همراه با مدل های توانمند مربوطه در مرحله طراحی سیستم توسعه یافته و به کار رفته اند، افزون بر این در صورت داشتن مدلی مناسب، این مدل از فقدان یک رویکرد توانمند چک کردن مدل نیز رنج می برد. برای مقابله با عدم قطعیت در پارادایم وارسی مدل، این مقاله یک مدل کریپکه فازی (FzKripke) را معرفی نموده و سپس یک رویکرد راستی آزمایی را با استفاده از منطق جدیدی به نام منطق درخت محاسبات فازی* (FzCTL*) ارائه می نماید. نه تنها با استفاده از مفاهیم شناخته شده ای مانند: تجرید و شبیه سازی دو گانه به مساله انفجار فضای حالت پرداخته شده بلکه یک روش تقریبی نیز به عنوان تکنیکی جدید برای مقابله با این مشکل ارائه گشته است. هم چنین نمودار برنامه فازی، که تعمیمی از نمودار برنامه و FzKripke محسوب می شود، در این مقاله با توجه به سطح بالاتر تجرید در ساخت مدل معرفی شده است. نهایتاً به منظور نشان دادن قابلیت مدل های پیشنهادی، مدلسازی و راستی آزمایی یک فلیپ فلاپ چند مقداری مورد مطالعه قرار گرفته است.
1. مقدمه
چک کردن یا وارسی مدل یک تکنیک صوری خودکار برای بررسی خواص مربوط به صحت سیستم می باشد، به طور خاص وارسی مدل که وارسی خواص نیز خوانده می شود به مساله زیر اطلاق می گردد: "با توجه به مدل حالت محدود و خواص صوری، چک کردن مدل به بررسی خودکار برقراری خواص مزبور در آن مدل می پردازد" [BK]. خواص زمانی سیستم های واکنشی یا انفعالی را تنها می توان با وارسی مدل زمانی بررسی نمود. در این مدل ها، زمان به دو صورت: پیوسته (زمان واقعی) و یا گسسته لحاظ می گردد. به منظور بررسی اغلب مدل های زمان واقعی همانند: اتوماتای بهنگام (TA) [AD94]، تبدیل این مدل ها به مدل های زمانی گسسته و سپس اجرای فرآیند وارسی مدل با بکارگیری منطق های ساده تر مانند منطق درخت محاسبات (CTL) ضرورت دارد. علت این امر آن است که تعریف منطق در کنار مدل های زمانی پیوسته ای از قبیل: منطق درخت محاسبات بهنگام (TCTL) قابلیت مشارکت در فرآیند چک کردن یا وارسی مدل را ندارد.
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.
1. Introduction
Model checking is an automatic formal technique for investigating correctness properties of systems, more specifically model checking also known as property checking refers to the following problem: “Given a finite-state model and a formal property, model checking automatically checks whether this property holds for that model” [BK]. Temporal properties of reactive systems can only be checked by temporal model checking. In these models, time is considered as either concrete (real-time) or discrete. In order to check the majority of real-time models such as timed automata (TA) [AD94], it is necessary to convert these models into discrete time models and then perform model checking process employing simpler logics such as computation tree logic (CTL). It is because logics defined alongside concrete time models such as timed computation tree logic (TCTL) are incapable of participating in model checking process.
چکیده
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. نتیجه گیری و کارهای آتی
منابع
Abstract
1. Introduction
2. Background
2.1. Model checking
2.2. Modal logic
2.3. Temporal logic generalizations
2.4. Fuzzy logic
2.5. Fuzzy transition-nondeterministic finite automata
3. Fuzzy Kripke model
4. Fuzzy CTL∗
5. Approximability of FzCTL temporal properties on FzKripke
6. Fuzzy Kripke abstraction and abstracted model approximation
6.1. Bisimulation equivalence
7. Fuzzy Program Graph
7.1. Simple Fuzzy Program Graph
7.2. Equivalency between Fuzzy Program Graph and Fuzzy Kripke
8. From FzPG to corresponding abstracted and approximated FzKripke
8.1. Normal -approximable formula
9. Case study
10. Conclusion and future work
- ترجمه فارسی مقاله با فرمت ورد (word) با قابلیت ویرایش، بدون آرم سایت ای ترجمه
- ترجمه فارسی مقاله با فرمت pdf، بدون آرم سایت ای ترجمه