کد مقاله | کد نشریه | سال انتشار | مقاله انگلیسی | نسخه تمام متن |
---|---|---|---|---|
10331269 | 686658 | 2005 | 5 صفحه PDF | دانلود رایگان |
عنوان انگلیسی مقاله ISI
A quadratic-time DBM-based successor algorithm for checking timed automata
دانلود مقاله + سفارش ترجمه
دانلود مقاله ISI انگلیسی
رایگان برای ایرانیان
موضوعات مرتبط
مهندسی و علوم پایه
مهندسی کامپیوتر
نظریه محاسباتی و ریاضیات
پیش نمایش صفحه اول مقاله
چکیده انگلیسی
Most of the timed automaton model checking algorithms explore state spaces by enumeration of time zones. The data structure called Difference Bound Matrix (DBM) is widely adopted to represent time zones because of its efficiency and simplicity. In this paper, we first present a quadratic-time algorithm to compute the canonical form of the conjunction of a canonical DBM and a time guard or a location invariant. Based on this algorithm, we present a quadratic-time DBM-based successor algorithm for timed automaton model checking.
ناشر
Database: Elsevier - ScienceDirect (ساینس دایرکت)
Journal: Information Processing Letters - Volume 96, Issue 3, 15 November 2005, Pages 101-105
Journal: Information Processing Letters - Volume 96, Issue 3, 15 November 2005, Pages 101-105
نویسندگان
Jianhua Zhao, Xuandong Li, Guoliang Zheng,