License: Creative Commons Attribution 3.0 Unported license (CC BY 3.0)
When quoting this document, please refer to the following
DOI: 10.4230/LIPIcs.FSTTCS.2016.28
URN: urn:nbn:de:0030-drops-68639
URL: http://dagstuhl.sunsite.rwth-aachen.de/volltexte/2016/6863/
Go to the corresponding LIPIcs Volume Portal

Weinert, Alexander ; Zimmermann, Martin

Visibly Linear Dynamic Logic

pdf-format:
LIPIcs-FSTTCS-2016-28.pdf (0.5 MB)

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.

BibTeX - Entry

@InProceedings{weinert_et_al:LIPIcs:2016:6863,
  author =	{Alexander Weinert and Martin Zimmermann},
  title =	{{Visibly Linear Dynamic Logic}},
  booktitle =	{36th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2016)},
  pages =	{28:1--28:14},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-027-9},
  ISSN =	{1868-8969},
  year =	{2016},
  volume =	{65},
  editor =	{Akash Lal and S. Akshay and Saket Saurabh and Sandeep Sen},
  publisher =	{Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{http://drops.dagstuhl.de/opus/volltexte/2016/6863},
  URN =		{urn:nbn:de:0030-drops-68639},
  doi =		{10.4230/LIPIcs.FSTTCS.2016.28},
  annote =	{Keywords: Temporal Logic, Visibly Pushdown Languages, Satisfiability, Model Checking, Infinite Games}
}

Keywords: Temporal Logic, Visibly Pushdown Languages, Satisfiability, Model Checking, Infinite Games
Collection: 36th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2016)
Issue Date: 2016
Date of publication: 10.12.2016

DROPS-Home | Fulltext Search | Imprint | Privacy Published by LZI