کد مقاله کد نشریه سال انتشار مقاله انگلیسی نسخه تمام متن
423289 685198 2006 18 صفحه PDF دانلود رایگان
عنوان انگلیسی مقاله ISI
Liveness Checking as Safety Checking for Infinite State Spaces
موضوعات مرتبط
مهندسی و علوم پایه مهندسی کامپیوتر نظریه محاسباتی و ریاضیات
پیش نمایش صفحه اول مقاله
Liveness Checking as Safety Checking for Infinite State Spaces
چکیده انگلیسی

In previous work we have developed a syntactic reduction of repeated reachability to reachability for finite state systems. This may lead to simpler and more uniform proofs for model checking of liveness properties, help to find shortest counterexamples, and overcome limitations of closed-source model-checking tools. In this paper we show that a similar reduction can be applied to a number of infinite state systems, namely, (ω−)regular model checking, push-down systems, and timed automata.

ناشر
Database: Elsevier - ScienceDirect (ساینس دایرکت)
Journal: Electronic Notes in Theoretical Computer Science - Volume 149, Issue 1, 3 February 2006, Pages 79-96