مشخصات کتاب

Integrating Decision Procedures for Temporal Verification

ویرایش:  
نویسندگان: Nikolaj Skallerud Bjorner  
سری:  
ISBN (شابک) : 9780599239845 
ناشر: Stanford University 
سال نشر: 1999 
تعداد صفحات: 181 
زبان: English 
فرمت فایل : PDF (درصورت درخواست کاربر به PDF، EPUB یا AZW3 تبدیل می شود) 
حجم فایل: 1 مگابایت 

در صورت تبدیل فایل کتاب Integrating Decision Procedures for Temporal Verification به فرمت های PDF، EPUB، AZW3، MOBI و یا DJVU می توانید به پشتیبان اطلاع دهید تا فایل مورد نظر را تبدیل نمایند.

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

توضیحاتی در مورد کتاب یکپارچه سازی رویه های تصمیم گیری برای تأیید موقت

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

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

This thesis concentrates on the development of decision procedures to tackle challenges met in the combination of model checking, abstract interpretation and deductive methods for verification of reactive systems. Proof-obligations are here often formulated using operations from different theories. For parameterized programs and real-time systems, verification conditions also often include quantifiers, so ground reasoning is not enough; pure first-order reasoning is on the other hand outperformed by specialized constraint solvers, such as linear programming techniques. We aim at combining quantifier reasoning with decision procedures. For this purpose this thesis presents decision procedures for quantifier-free logics which are combined into a general validity checker by maintaining constraints incrementally. This is extended to first-order reasoning using rigid E -unification procedures. We use a new congruence closure algorithm for the integration of decision procedures. One of its attractive features is that it can tightly integrate theories over co-recursive data types. We also show how the congruence closure algorithm is extended to support special relations. An attractive feature of combining decision procedures within a congruence closure algorithm is a tight and therefore efficient integration. The approach is however essentially limited to theories that are solvable . In solvable theories all implied equalities can be summarized using substitutions. The limitation naturally challenges this as a basis for combining decision procedures. By presenting a spectrum of decision procedures that can be integrated in the framework we give evidence for the wide scope of this approach: an extension of Fourier's algorithm for quantifier elimination of linear arithmetical expressions, which extracts implicitly implied equalities on the fly, tightly integrated with a partial decision procedure for non-linear arithmetic; decision procedures for both recursive and co-recursive data types, including subterm relations and a length measure for recursive data-types; an algorithm for deciding a class of equational constraints between non-fixed size bit-vectors; and algorithms for reasoning about constraints over queues (lists where elements can be added to the front and the back), including sub-queue, prefix, suffix relations and support for length measures. The decision procedures have been used in STeP, the Stanford Temporal Prover, and we report on experience on verification examples.

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

کتاب های تصادفی

دانلود کتاب Innere Medizin

دانلود کتاب Perspectives on Initiation

دانلود کتاب Critical Approaches to the History of Western Herbal Medicine: From Classical Antiquity to the Early Modern Period

دانلود کتاب Aux origines du nationalisme turc: Yusuf Akçura, 1876-1935

دانلود کتاب Fevered Planet: How Diseases Emerge When We Harm Nature