Parametric Linear Dynamic Logic

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.

Authors

• Peter Faymonville
• Martin Zimmermann

Keywords

• Linear Temporal Logic
• Linear Dynamic Logic
• Parametric Linear Temporal Logic
• Model checking
• Realizability