Parametric Linear Dynamic Logic (full version)

TL;DR

This paper introduces Parametric Linear Dynamic Logic (PLDL), an extension of LDL with parameters for timing constraints, enabling the expression of all omega-regular properties and providing efficient algorithms for model checking and realizability.

Contribution

The paper presents the first translation of PLDL into nondeterministic Büchi automata and establishes complexity bounds for model checking and realizability problems.

Findings

PLDL can express all omega-regular properties with timing constraints.

Model checking and realizability for PLDL are complete for exponential and doubly-exponential time classes.

Provides tight bounds on optimal parameter values for model checking and realizability.

Abstract

We introduce Parametric Linear Dynamic Logic (PLDL), which extends Linear Dynamic Logic (LDL) by temporal operators equipped with parameters that bound their scope. LDL itself was proposed as an extension of Linear Temporal Logic (LTL) that is able to express all omega-regular specifications while still maintaining many of LTL's desirable properties like intuitive syntax and semantics and a translation into non-deterministic B\"uchi 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 omega-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\"uchi automata of exponential size via alternating automata. This yields polynomial space algorithms for model checking and assume-guarantee model checking and a realizability algorithm with doubly-exponential running time. All three problems are also shown to be complete for these complexity classes. Moreover, we give tight upper and lower bounds on optimal parameter values for model checking and realizability. Using these bounds, we present a polynomial space procedure for model checking optimization and an algorithm with triply-exponential running time for realizability optimization. Our results show that PLDL model checking and realizability are no harder than their respective (parametric) LTL counterparts.