ورود به حساب

نام کاربری گذرواژه

گذرواژه را فراموش کردید؟ کلیک کنید

حساب کاربری ندارید؟ ساخت حساب

ساخت حساب کاربری

نام نام کاربری ایمیل شماره موبایل گذرواژه

برای ارتباط با ما می توانید از طریق شماره موبایل زیر از طریق تماس و پیامک با ما در ارتباط باشید


09117307688
09117179751

در صورت عدم پاسخ گویی از طریق پیامک با پشتیبان در ارتباط باشید

دسترسی نامحدود

برای کاربرانی که ثبت نام کرده اند

ضمانت بازگشت وجه

درصورت عدم همخوانی توضیحات با کتاب

پشتیبانی

از ساعت 7 صبح تا 10 شب

دانلود کتاب Verifying Temporal Properties of Systems

دانلود کتاب تأیید ویژگی های زمانی سیستم ها

Verifying Temporal Properties of Systems

مشخصات کتاب

Verifying Temporal Properties of Systems

ویرایش: 1 
نویسندگان:   
سری: Progress in Theoretical Computer Science 
ISBN (شابک) : 9781468468212, 9781468468199 
ناشر: Birkhäuser Basel 
سال نشر: 1992 
تعداد صفحات: 122 
زبان: English 
فرمت فایل : PDF (درصورت درخواست کاربر به PDF، EPUB یا AZW3 تبدیل می شود) 
حجم فایل: 3 مگابایت 

قیمت کتاب (تومان) : 45,000



کلمات کلیدی مربوط به کتاب تأیید ویژگی های زمانی سیستم ها: است



ثبت امتیاز به این کتاب

میانگین امتیاز به این کتاب :
       تعداد امتیاز دهندگان : 18


در صورت تبدیل فایل کتاب Verifying Temporal Properties of Systems به فرمت های PDF، EPUB، AZW3، MOBI و یا DJVU می توانید به پشتیبان اطلاع دهید تا فایل مورد نظر را تبدیل نمایند.

توجه داشته باشید کتاب تأیید ویژگی های زمانی سیستم ها نسخه زبان اصلی می باشد و کتاب ترجمه شده به فارسی نمی باشد. وبسایت اینترنشنال لایبرری ارائه دهنده کتاب های زبان اصلی می باشد و هیچ گونه کتاب ترجمه شده یا نوشته شده به فارسی را ارائه نمی دهد.


توضیحاتی در مورد کتاب تأیید ویژگی های زمانی سیستم ها



هدف این تک نگاری ارائه یک تکنیک قوی برای اثبات همه منظوره برای تأیید سیستم ها، اعم از متناهی یا نامتناهی است. این ایده بررسی مدل محلی محدود را که توسط استرلینگ و واکر معرفی شد، گسترش می‌دهد: به جای پیمایش کل فضای حالت یک مدل، همانطور که برای بررسی مدل به معنای امرسون، کلارک و همکاران انجام می‌شود. (بررسی اینکه آیا یک مدل (متناهی) یک فرمول را برآورده می کند)، بررسی مدل محلی می پرسد که آیا یک حالت خاص یک فرمول را برآورده می کند یا خیر، و فقط حالت های نزدیک را به اندازه کافی برای پاسخ به آن سؤال بررسی می کند. تکنیک مورد استفاده، روش تابلویی بود، ساخت تابلو بر اساس فرمول و ساختار محلی مدل. این تکنیک تابلو در اینجا با در نظر گرفتن مجموعه ای از حالات، به جای حالت های منفرد، به حالت بی نهایت تعمیم داده می شود. از آنجایی که منطق مورد استفاده، حساب مدال گزاره ای، اتصالات مدال و بولی ساده را از عملگرهای نقطه ثابت قدرتمند جدا می کند (که منطق را از بسیاری از منطق های زمانی دیگر گویاتر می کند)، می توان مجموعه ای نسبتاً ساده از قوانین ارائه داد. برای ساخت تابلو بسیاری از ظرافت‌ها از خود تابلو حذف می‌شود، و در رابطه با فضای حالت تعریف‌شده توسط تابلو قرار می‌گیرد- موفقیت تابلو بستگی به پایه و اساس این رابطه دارد. تکنیک تابلوی تعمیم‌یافته در شبکه‌های پتری به نمایش گذاشته شده است، و مفاهیم استاندارد مختلف از تئوری شبکه نقش مهمی در استفاده از این تکنیک در شبکه‌ها دارد - به‌ویژه، حساب ثابت نقش مهمی دارد.


توضیحاتی درمورد کتاب به خارجی

This monograph aims to provide a powerful general-purpose proof tech­ nique for the verification of systems, whether finite or infinite. It extends the idea of finite local model-checking, which was introduced by Stirling and Walker: rather than traversing the entire state space of a model, as is done for model-checking in the sense of Emerson, Clarke et ai. (checking whether a (finite) model satisfies a formula), local model-checking asks whether a particular state satisfies a formula, and only explores the nearby states far enough to answer that question. The technique used was a tableau method, constructing a tableau according to the formula and the local structure of the model. This tableau technique is here generalized to the infinite case by considering sets of states, rather than single states; because the logic used, the propositional modal mu-calculus, separates simple modal and boolean connectives from powerful fix-point operators (which make the logic more expressive than many other temporal logics), it is possible to give a rela­ tively straightforward set of rules for constructing a tableau. Much of the subtlety is removed from the tableau itself, and put into a relation on the state space defined by the tableau-the success of the tableau then depends on the well-foundedness of this relation. The generalized tableau technique is exhibited on Petri nets, and various standard notions from net theory are shown to playa part in the use of the technique on nets-in particular, the invariant calculus has a major role.



فهرست مطالب

Front Matter....Pages i-viii
Introduction....Pages 1-13
Program Logics and the Mu-Calculus....Pages 14-29
The Tableau System....Pages 30-50
Applications to Nets....Pages 51-84
The Complexity of Mu-Formulae on Nets....Pages 85-100
Conclusions and Further Work....Pages 101-104
Back Matter....Pages 105-115




نظرات کاربران