کد مقاله | کد نشریه | سال انتشار | مقاله انگلیسی | نسخه تمام متن |
---|---|---|---|---|
426409 | 686052 | 2015 | 34 صفحه PDF | دانلود رایگان |
عنوان انگلیسی مقاله ISI
Taming past LTL and flat counter systems
ترجمه فارسی عنوان
سیستم های ضد شمار و سیستم های ضد تخت را ترسانده است
دانلود مقاله + سفارش ترجمه
دانلود مقاله ISI انگلیسی
رایگان برای ایرانیان
کلمات کلیدی
منطق زمانی منطقی، لکنت زبان، مدل چک کردن، سیستم ضد، تخت پیچیدگی، سیستم معادلات، راه حل کوچک، محاسبات فورببرگر
موضوعات مرتبط
مهندسی و علوم پایه
مهندسی کامپیوتر
نظریه محاسباتی و ریاضیات
چکیده انگلیسی
Reachability and LTL model-checking problems for flat counter systems are known to be decidable but whereas the reachability problem can be shown in NP, the best known complexity upper bound for the latter problem is made of a tower of several exponentials. Herein, we show that this problem is only NP-complete even if LTL admits past-time operators and arithmetical constraints on counters. As far as past-time operators are concerned, their addition to LTL immediately leads to complications and hence an NP upper bound cannot be deduced by translating formulae into LTL and studying the problem only for this latter logic. We also provide other complexity results obtained by restricting further the class of flat counter systems.
ناشر
Database: Elsevier - ScienceDirect (ساینس دایرکت)
Journal: Information and Computation - Volume 242, June 2015, Pages 306–339
Journal: Information and Computation - Volume 242, June 2015, Pages 306–339
نویسندگان
Stéphane Demri, Amit Kumar Dhar, Arnaud Sangnier,