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

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

عنوان فارسی مقاله: تجرید و تقریب در منطق و مدل های زمانی فازی
عنوان انگلیسی مقاله: Abstraction and approximation in fuzzy temporal logics and models
مجله/کنفرانس: جنبه های رسمی محاسبات - Formal Aspects of Computing
رشته های تحصیلی مرتبط: مهندسی کامپیوتر
گرایش های تحصیلی مرتبط: رایانش ابری، معماری سیستم های کامپیوتری
کلمات کلیدی فارسی: تجرید، تقریب، مدل کریپکـه فازی، منطق زمانی فازی، چک کردن یا وارسی مدل، نمودار برنامه فازی، فلیپ فلاپ چند مقداری
کلمات کلیدی انگلیسی: Abstraction - Approximation - Fuzzy Kripke model - Fuzzy temporal logic - Model checking - Fuzzy program graph - Multi-valued flip-flop
نوع نگارش مقاله: مقاله پژوهشی (Research Article)
نمایه: scopus - master journals - JCR
شناسه دیجیتال (DOI): https://doi.org/10.1007/s00165-014-0318-7
دانشگاه: گروه مهندسی کامپیوتر ، دانشگاه آزاد اسلامی (واحد علوم و تحقیقات) ، تهران ، ایران
ناشر: اسپرینگر - Springer
نوع ارائه مقاله: ژورنال
نوع مقاله: ISI
سال انتشار مقاله: 2014
ایمپکت فاکتور: 1.730 در سال 2018
شاخص H_index: 36 در سال 2019
شاخص SJR: 0.430 در سال 2018
شناسه ISSN: 0934-5043
شاخص Quartile (چارک): Q3 در سال 2018
صفحات مقاله انگلیسی: 26
صفحات ترجمه فارسی: 41 (شامل 1 صفحه رفرنس انگلیسی)
فرمت مقاله انگلیسی: PDF
فرمت ترجمه فارسی: ورد و pdf
مشخصات ترجمه: تایپ شده با فونت B Nazanin 14
ترجمه شده از: انگلسی به فارسی
وضعیت ترجمه: ترجمه شده و آماده دانلود
آیا این مقاله بیس است: بله
آیا این مقاله مدل مفهومی دارد: دارد
آیا این مقاله پرسشنامه دارد: ندارد
آیا این مقاله متغیر دارد: ندارد
آیا منابع داخل متن درج یا ترجمه شده است: خیر
آیا توضیحات زیر تصاویر و جداول ترجمه شده است: بله
آیا متون داخل تصاویر و جداول ترجمه شده است: بله
کد محصول: 9854
رفرنس: دارای رفرنس در داخل متن و انتهای مقاله
رفرنس در ترجمه: در انتهای مقاله درج شده است
ترجمه فارسی فهرست مطالب

چکیده


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

نمونه ترجمه فارسی مقاله

چکیده


اخیراً، با تعریف منطق زمانی فازی مناسب، خواص زمانی سیستم های دینامیکی در خلال فرآیند چک کردن یا وارسی مدل مشخص شده اند و در عین حال تعداد کمی از منطق های زمانی فازی همراه با مدل های توانمند مربوطه در مرحله طراحی سیستم توسعه یافته و به کار رفته اند، افزون بر این در صورت داشتن مدلی مناسب، این مدل از فقدان یک رویکرد توانمند چک کردن مدل نیز رنج می برد. برای مقابله با عدم قطعیت در پارادایم وارسی مدل، این مقاله یک مدل کریپکه فازی (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.

محتوای این محصول:
- اصل مقاله انگلیسی با فرمت pdf
- ترجمه فارسی مقاله با فرمت ورد (word) با قابلیت ویرایش، بدون آرم سایت ای ترجمه
- ترجمه فارسی مقاله با فرمت pdf، بدون آرم سایت ای ترجمه
قیمت محصول: ۲۸,۰۰۰ تومان
خرید محصول
  • اشتراک گذاری در

دیدگاه خود را بنویسید:

تاکنون دیدگاهی برای این نوشته ارسال نشده است

تجرید و تقریب در منطق و مدل های زمانی فازی
مشاهده خریدهای قبلی
نوشته های مرتبط
مقالات جدید
لوگوی رسانه های برخط

logo-samandehi

پیوندها