Parametric linear dynamic logic
From MaRDI portal
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 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"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 -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 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.
Recommendations
- Parametric linear dynamic logic
- Visibly linear dynamic logic
- Visibly linear dynamic logic
- Parametrized logic programming
- Weighted linear dynamic logic
- Publication:4941925
- Dynamic composition of parameterised logic modules
- Parametric logic: Foundations
- STRUCTURED NONSTANDARD DYNAMIC LOGIC
- scientific article; zbMATH DE number 1086632
Cites work
- Alternating finite automata on -words
- Antichains and compositional algorithms for LTL synthesis
- FINITE STATE PROCESSES, Z-TEMPORAL LOGIC AND THE MONADIC THEORY OF THE INTEGERS
- From liveness to promptness
- scientific article; zbMATH DE number 3926220 (Why is no real title available?)
- scientific article; zbMATH DE number 4124989 (Why is no real title available?)
- scientific article; zbMATH DE number 2080056 (Why is no real title available?)
- scientific article; zbMATH DE number 1796123 (Why is no real title available?)
- Observations on determinization of Büchi automata
- Optimal bounds in parametric LTL games
- Parametric linear dynamic logic
- Parametric metric interval temporal logic
- Parametric temporal logic for “model measuring”
- Programming Techniques: Regular expression search algorithm
- Propositional dynamic logic of regular programs
- Reasoning about infinite computations
- Regular Linear Temporal Logic
- Solving Sequential Conditions by Finite-State Strategies
- Temporal logic can be more expressive
- The complexity of propositional linear temporal logics
- Tighter Bounds for the Determinisation of Büchi Automata
Cited in
(19)- Distributed synthesis for parameterized temporal logics
- Visibly linear dynamic logic
- Some results on parametric temporal logic
- Almost event-rate independent monitoring
- A survey of challenges for runtime verification from advanced application domains (beyond software)
- Quantitative reductions and vertex-ranked infinite games
- Incorporating monitors in reactive synthesis without paying the price
- Parameterized linear temporal logics meet costs: still not costlier than LTL
- Robust, expressive, and quantitative linear temporal logics: pick any two for free
- Delay games with WMSO+U winning conditions
- Quantitative reductions and vertex-ranked infinite games
- Parametric temporal logic for “model measuring”
- A parametrized propositional dynamic logic with application to service synthesis
- scientific article; zbMATH DE number 1405643 (Why is no real title available?)
- Parametric linear dynamic logic
- Parameterized linear temporal logics meet costs: still not costlier than LTL
- Robust, expressive, and quantitative linear temporal logics: pick any two for free
- Optimal strategies in weighted limit games
- Propositional Dynamic Logic for Hyperproperties
This page was built for publication: Parametric linear dynamic logic
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q515660)
