کد مقاله | کد نشریه | سال انتشار | مقاله انگلیسی | نسخه تمام متن |
---|---|---|---|---|
10330804 | 686142 | 2005 | 39 صفحه PDF | دانلود رایگان |
عنوان انگلیسی مقاله ISI
Decidable first-order transition logics for PA-processes
دانلود مقاله + سفارش ترجمه
دانلود مقاله ISI انگلیسی
رایگان برای ایرانیان
کلمات کلیدی
موضوعات مرتبط
مهندسی و علوم پایه
مهندسی کامپیوتر
نظریه محاسباتی و ریاضیات
پیش نمایش صفحه اول مقاله
چکیده انگلیسی
We show the decidability of model checking PA-processes against several first-order logics based upon the reachability predicate. The main tool for this result is the recognizability by tree automata of the reachability relation. The tree automata approach and the transition logics we use allow a smooth and general treatment of parameterized model checking for PA. This approach is extended to handle a quite general notion of costs of PA-steps. In particular, when costs are Parikh images of traces, we show decidability of a transition logic extended by some form of first-order reasoning over costs.
ناشر
Database: Elsevier - ScienceDirect (ساینس دایرکت)
Journal: Information and Computation - Volume 203, Issue 1, 25 November 2005, Pages 75-113
Journal: Information and Computation - Volume 203, Issue 1, 25 November 2005, Pages 75-113
نویسندگان
Denis Lugiez, Philippe Schnoebelen,