کد مقاله | کد نشریه | سال انتشار | مقاله انگلیسی | نسخه تمام متن |
---|---|---|---|---|
6873959 | 686072 | 2015 | 45 صفحه PDF | دانلود رایگان |
عنوان انگلیسی مقاله ISI
An SMT-based approach to satisfiability checking of MITL
دانلود مقاله + سفارش ترجمه
دانلود مقاله ISI انگلیسی
رایگان برای ایرانیان
موضوعات مرتبط
مهندسی و علوم پایه
مهندسی کامپیوتر
نظریه محاسباتی و ریاضیات
پیش نمایش صفحه اول مقاله
![عکس صفحه اول مقاله: An SMT-based approach to satisfiability checking of MITL An SMT-based approach to satisfiability checking of MITL](/preview/png/6873959.png)
چکیده انگلیسی
We present a satisfiability-preserving reduction from MITL interpreted over finitely-variable continuous behaviors to Constraint LTL over clocks, a variant of CLTL that is decidable, and for which an SMT-based bounded satisfiability checker is available. The result is a new complete and effective decision procedure for MITL. Although decision procedures for MITL already exist, the automata-based techniques they employ appear to be very difficult to realize in practice, and, to the best of our knowledge, no implementation currently exists for them. A prototype tool for MITL based on the encoding presented here has, instead, been implemented and is publicly available.
ناشر
Database: Elsevier - ScienceDirect (ساینس دایرکت)
Journal: Information and Computation - Volume 245, December 2015, Pages 72-97
Journal: Information and Computation - Volume 245, December 2015, Pages 72-97
نویسندگان
Marcello M. Bersani, Matteo Rossi, Pierluigi San Pietro,