Faymonville, Peter and Zimmermann, Martin 
ORCID: 0000-0002-8038-2453
(2017)
Parametric Linear Dynamic Logic.
Information and Computation, 253 (Part 2).
pp. 237-256.
|
Text
pldl_journal.pdf - Author Accepted Manuscript Download (467kB) | Preview |
Abstract
We introduce Parametric Linear Dynamic Logic (PLDL), which extends Linear Dynamic Logic (LDL) by adding temporal operators equipped with parameters that bound their scope. LDL is an extension of Linear Temporal Logic (LTL) to all ω-regular specifications, while maintaining a translation into exponentially-sized non-deterministic Büchi automata. Since LDL cannot express timing constraints, we add parameterized operators and subsume parameterized extensions of LTL like Parametric LTL and PROMPT-LTL. Our contribution is a translation of PLDL into exponentially-sized non-deterministic Büchi automata via alternating automata. This yields PSPACE algorithms for model checking and assume-guarantee model checking and a 2EXPTIME realizability algorithm. The problems are complete for their complexity classes. We give tight bounds on optimal parameter values for model checking and realizability and present a PSPACE procedure for model checking optimization and a 3EXPTIME algorithm for realizability optimization. Our results show that these PLDL problems are no harder than their (parametric) LTL counterparts.
| Item Type: | Article |
|---|---|
| Uncontrolled Keywords: | Linear Temporal Logic, Linear Dynamic Logic, Parametric Linear Temporal Logic, Model checking, Realizability |
| Depositing User: | Symplectic Admin |
| Date Deposited: | 15 Jul 2019 12:51 |
| Last Modified: | 19 Jan 2023 00:37 |
| DOI: | 10.1016/j.ic.2016.07.009 |
| Related URLs: | |
| URI: | https://livrepository.liverpool.ac.uk/id/eprint/3050010 |
Dimensions
Dimensions
