Document Open Access Logo

Visibly Linear Dynamic Logic

Authors Alexander Weinert, Martin Zimmermann

PDF
Thumbnail PDF

File

LIPIcs.FSTTCS.2016.28.pdf
  • Filesize: 0.54 MB
  • 14 pages

Document Identifiers

Author Details

Alexander Weinert
Martin Zimmermann

Cite As Get BibTex

Alexander Weinert and Martin Zimmermann. Visibly Linear Dynamic Logic. In 36th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2016). Leibniz International Proceedings in Informatics (LIPIcs), Volume 65, pp. 28:1-28:14, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2016) https://doi.org/10.4230/LIPIcs.FSTTCS.2016.28

Abstract

We introduce Visibly Linear Dynamic Logic (VLDL), which extends Linear Temporal Logic (LTL) by temporal operators that are guarded by visibly pushdown languages over finite words. In VLDL one can, e.g., express that a function resets a variable to its original value after its execution, even in the presence of an unbounded number of intermediate recursive calls. We prove that VLDL describes exactly the omega-visibly pushdown languages. Thus it is strictly more expressive than LTL and able to express recursive properties of programs with unbounded call stacks.

The main technical contribution of this work is a translation of VLDL into omega-visibly pushdown automata 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 prove all these problems to be complete for their respective complexity classes.

Subject Classification

Keywords
  • Temporal Logic
  • Visibly Pushdown Languages
  • Satisfiability
  • Model Checking
  • Infinite Games

Metrics

  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    0
    PDF Downloads
    0
    Metadata Views

References

  1. Rajeev Alur, Kousha Ettesami, and Parthasarathy Madhusudan. A temporal logic of nested calls and returns. In TACAS 2004, volume 2988 of LNCS, pages 467-481. Springer, 2004. Google Scholar
  2. Rajeev Alur and Parthasarathy Madhusudan. Visibly Pushdown Languages. In STOC 2004, pages 202-211. ACM, 2004. Google Scholar
  3. Ahmed Bouajjani, Javier Esparza, and Oded Maler. Reachability analysis of pushdown automata: Application to model-checking. In A. Mazurkiewicz and J. Winkowski, editors, CONCUR 1997, volume 1243 of LNCS, pages 135-150. Springer, 1997. Full version available at http://www.liafa.univ-paris-diderot.fr/~abou/BEM97.pdf.
  4. Laura Bozzelli. Alternating Automata and a Temporal Fixpoint Calculus for Visibly Pushdown Languages. In L. Caires and V. T. Vasconcelos, editors, CONCUR 2007, volume 4703 of LNCS, pages 476-491. Springer, 2007. Google Scholar
  5. Laura Bozzelli and César Sánchez. Visibly linear temporal logic. In IJCAR 2014, volume 8562 of LNCS, pages 418-483, 2014. Google Scholar
  6. Peter Faymonville and Martin Zimmermann. Parametric Linear Dynamic Logic. Inf. Comput., 2016. Article in press. Google Scholar
  7. Martin Leucker and César Sanchéz. Regular linear temporal logic. In C. B. Jones, Z. Liu, and J. Woodcock, editors, ICTAC 2007, number 4711 in LNCS, pages 291-305, 2007. Google Scholar
  8. Christof Löding, Parthasarathy Madhusudan, and Olivier Serre. Visibly Pushdown Games. In L. Lodaya and M. Mahajan, editors, FSTTCS 2004, volume 3328 of LNCS, pages 408-420. Springer, 2005. Google Scholar
  9. Amir Pnueli. The temporal logic of programs. In FOCS 1977, pages 46-57. IEEE, 1977. Google Scholar
  10. Moshe Vardi. The Rise and Fall of LTL. In G. D'Agostino and S. La Torre, editors, EPTCS 54, 2011. Google Scholar
  11. Moshe Vardi and Pierre Wolper. Reasoning about infinite computations. Inf. and Comp., 115:1-37, 1994. Google Scholar
  12. Alexander Weinert and Martin Zimmermann. Visibly linear dynamic logic. arXiv, 1512.05177, 2015. Google Scholar
  13. Pierre Wolper. Temporal logic can be more expressive. Inf. and Cont., 56:72-99, 1983. Google Scholar
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail
© 2023-2024 Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact