Parametric Linear Dynamic Logic
We introduce Parametric Linear Dynamic Logic (PLDL), which extends Linear Dynamic Logic (LDL) by temporal operators equipped with parameters that bound their scope. LDL was proposed as an extension of Linear Temporal Logic (LTL) that is able to express all ω-regular specifications while still mainta...
| Main Authors: | , |
|---|---|
| Format: | Article |
| Language: | English |
| Published: |
Open Publishing Association
2014-08-01
|
| Series: | Electronic Proceedings in Theoretical Computer Science |
| Online Access: | http://arxiv.org/pdf/1408.5957v1 |
| _version_ | 1811308749132922880 |
|---|---|
| author | Peter Faymonville Martin Zimmermann |
| author_facet | Peter Faymonville Martin Zimmermann |
| author_sort | Peter Faymonville |
| collection | DOAJ |
| description | We introduce Parametric Linear Dynamic Logic (PLDL), which extends Linear Dynamic Logic (LDL) by temporal operators equipped with parameters that bound their scope. LDL was proposed as an extension of Linear Temporal Logic (LTL) that is able to express all ω-regular specifications while still maintaining many of LTL's desirable properties like an intuitive syntax and a translation into non-deterministic Büchi automata of exponential size. But LDL lacks capabilities to express timing constraints. By adding parameterized operators to LDL, we obtain a logic that is able to express all ω-regular properties and that subsumes parameterized extensions of LTL like Parametric LTL and PROMPT-LTL. Our main technical contribution is a translation of PLDL formulas into non-deterministic Büchi word automata of exponential size via alternating automata. This yields a PSPACE model checking algorithm and a realizability algorithm with doubly-exponential running time. Furthermore, we give tight upper and lower bounds on optimal parameter values for both problems. These results show that PLDL model checking and realizability are not harder than LTL model checking and realizability. |
| first_indexed | 2024-04-13T09:28:57Z |
| format | Article |
| id | doaj.art-616049313f344473a9a647aa07d05d9b |
| institution | Directory Open Access Journal |
| issn | 2075-2180 |
| language | English |
| last_indexed | 2024-04-13T09:28:57Z |
| publishDate | 2014-08-01 |
| publisher | Open Publishing Association |
| record_format | Article |
| series | Electronic Proceedings in Theoretical Computer Science |
| spelling | doaj.art-616049313f344473a9a647aa07d05d9b2022-12-22T02:52:19ZengOpen Publishing AssociationElectronic Proceedings in Theoretical Computer Science2075-21802014-08-01161Proc. GandALF 2014607310.4204/EPTCS.161.8:26Parametric Linear Dynamic LogicPeter Faymonville0Martin Zimmermann1 Saarland University Saarland University We introduce Parametric Linear Dynamic Logic (PLDL), which extends Linear Dynamic Logic (LDL) by temporal operators equipped with parameters that bound their scope. LDL was proposed as an extension of Linear Temporal Logic (LTL) that is able to express all ω-regular specifications while still maintaining many of LTL's desirable properties like an intuitive syntax and a translation into non-deterministic Büchi automata of exponential size. But LDL lacks capabilities to express timing constraints. By adding parameterized operators to LDL, we obtain a logic that is able to express all ω-regular properties and that subsumes parameterized extensions of LTL like Parametric LTL and PROMPT-LTL. Our main technical contribution is a translation of PLDL formulas into non-deterministic Büchi word automata of exponential size via alternating automata. This yields a PSPACE model checking algorithm and a realizability algorithm with doubly-exponential running time. Furthermore, we give tight upper and lower bounds on optimal parameter values for both problems. These results show that PLDL model checking and realizability are not harder than LTL model checking and realizability.http://arxiv.org/pdf/1408.5957v1 |
| spellingShingle | Peter Faymonville Martin Zimmermann Parametric Linear Dynamic Logic Electronic Proceedings in Theoretical Computer Science |
| title | Parametric Linear Dynamic Logic |
| title_full | Parametric Linear Dynamic Logic |
| title_fullStr | Parametric Linear Dynamic Logic |
| title_full_unstemmed | Parametric Linear Dynamic Logic |
| title_short | Parametric Linear Dynamic Logic |
| title_sort | parametric linear dynamic logic |
| url | http://arxiv.org/pdf/1408.5957v1 |
| work_keys_str_mv | AT peterfaymonville parametriclineardynamiclogic AT martinzimmermann parametriclineardynamiclogic |