Name
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 ω-visibly pushdown languages, i.e., that it is strictly more expressive than LTL and able to express recursive properties of programs with unbounded call stacks. |
Year | DOI | Venue |
|---|---|---|
2015 | 10.1016/j.tcs.2018.06.030 | Theoretical Computer Science |
Keywords | DocType | Volume |
Temporal logic,Visibly pushdown languages,Satisfiability,Model checking,Infinite games | Journal | 747 |
ISSN | Citations | PageRank |
0304-3975 | 2 | 0.38 |
References | Authors | |
5 | 2 | |
Name | Order | Citations | PageRank |
|---|---|---|---|
| Alexander Weinert | 1 | 7 | 2.22 |
| Martin Zimmermann 0002 | 2 | 35 | 10.88 |