کد مقاله | کد نشریه | سال انتشار | مقاله انگلیسی | نسخه تمام متن |
---|---|---|---|---|
10330631 | 686051 | 2005 | 27 صفحه PDF | دانلود رایگان |
عنوان انگلیسی مقاله ISI
Bridging the gap between fair simulation and trace inclusion
دانلود مقاله + سفارش ترجمه
دانلود مقاله ISI انگلیسی
رایگان برای ایرانیان
موضوعات مرتبط
مهندسی و علوم پایه
مهندسی کامپیوتر
نظریه محاسباتی و ریاضیات
پیش نمایش صفحه اول مقاله
چکیده انگلیسی
The paper considers the problem of checking abstraction between two finite-state fair discrete systems. In automata-theoretic terms this is trace inclusion between two nondeterministic Streett automata. We propose to reduce this problem to an algorithm for checking fair simulation between two generalized Büchi automata. For solving this question we present a new triply nested μ-calculus formula which can be implemented by symbolic methods. We then show that every trace inclusion of this type can be solved by fair simulation, provided we augment the concrete system (the contained automaton) by an appropriate 'non-constraining' automaton. This establishes that fair simulation offers a complete method for checking trace inclusion for finite-state systems. We illustrate the feasibility of the approach by algorithmically checking abstraction between finite state systems whose abstraction could only be verified by deductive methods up to now.
ناشر
Database: Elsevier - ScienceDirect (ساینس دایرکت)
Journal: Information and Computation - Volume 200, Issue 1, 1 July 2005, Pages 35-61
Journal: Information and Computation - Volume 200, Issue 1, 1 July 2005, Pages 35-61
نویسندگان
Yonit Kesten, Nir Piterman, Amir Pnueli,