Academic Journal
An Automata-Theoretic Approach to Constraint LTL
| العنوان: | An Automata-Theoretic Approach to Constraint LTL |
|---|---|
| المؤلفون: | S. Demri, D. D'Souza |
| المساهمون: | The Pennsylvania State University CiteSeerX Archives |
| المصدر: | http://www.lsv.ens-cachan.fr/Publis/RAPPORTS_LSV/rr-lsv-2003-11.rr.ps. |
| سنة النشر: | 2003 |
| المجموعة: | CiteSeerX |
| مصطلحات موضوعية: | temporal logic, logics of space and time, model-checking |
| الوصف: | We consider an extension of linear-time temporal logic (LTL) with constraints interpreted over a concrete domain. We use a new automata-theoretic technique to show pspace decidability of the logic for the constraint systems (Z, <, =) and (N, <, =). Along the way, we give an automata-theoretic proof of a result of [BC02] when the constraint system D satisfies the completion property. Our decision procedures extend easily to handle extensions of the logic with past operators and constants, as well as an extension of the temporal language itself to monadic second order logic. Finally, we show that the logic. |
| نوع الوثيقة: | text |
| وصف الملف: | application/postscript |
| اللغة: | English |
| Relation: | http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.10.5502; http://www.lsv.ens-cachan.fr/Publis/RAPPORTS_LSV/rr-lsv-2003-11.rr.ps |
| الاتاحة: | http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.10.5502 http://www.lsv.ens-cachan.fr/Publis/RAPPORTS_LSV/rr-lsv-2003-11.rr.ps |
| Rights: | Metadata may be used without restrictions as long as the oai identifier remains attached to it. |
| رقم الانضمام: | edsbas.57E38BB1 |
| قاعدة البيانات: | BASE |
| الوصف غير متاح. |