Visibly Linear Dynamic Logic
Alexander Weinert, Martin Zimmermann
We introduce Visibly Linear Dynamic Logic (VLDL), which is an extension of Linear Dynamic Logic (LDL) with temporal operators that are guarded by nondeterministic visibly pushdown automata. We prove that VLDL describes exactly the visibly pushdown languages over infinite words, which makes it strictly more powerful than LTL and LDL and able to express properties of recursive programs. The main technical contribution of this work is a translation of VLDL formulas into nondeterministic visibly pushdown automata with Büchi acceptance of exponential size via one-way alternating jumping automata. This translation yields exponential-time algorithms for satisfiability, validity and model checking. We also show that visibly pushdown games with VLDL winning conditions are solvable in triply-exponential time. We show all of these problems to be complete for their respective complexity classes. Furthermore, we prove that using deterministic pushdown automata as guards yields undecidable decision problems.