Parametric Linear Dynamic Logic (full version)
Peter Faymonville, Martin Zimmermann

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…
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.
Taxonomy
TopicsFormal Methods in Verification · Logic, programming, and type systems · Model-Driven Software Engineering Techniques
