Author name cluster

Peter Faymonville

Possible papers associated with this exact author name in Arrow. This page groups case-insensitive exact name matches and is not a full identity disambiguation profile.

2 papers

1 author row

I&C Journal 2017 Journal Article

Parametric Linear Dynamic Logic

Peter Faymonville
Martin Zimmermann

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.

Details DOI

GandALF Workshop 2014 Workshop Paper

Parametric Linear Dynamic Logic

Peter Faymonville
Martin Zimmermann

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.

PDF Details DOI