# Visibly Linear Temporal Logic

We introduce a robust and tractable temporal logic, we call Visibly
Linear Temporal Logic (VLTL), which captures the full class of
Visibly Pushdown Languages. The novel logic avoids fix points and
provides instead natural temporal operators with simple and
intuitive semantics. We prove that the complexities of the
satisfiability and pushdown model checking problems are the same as
for other well known logics, like CARET and the nested word temporal
logic NWTL, which in contrast are strictly more limited in
expressive power than VLTL. Moreover, formulas of CARET and NWTL can
be easily and inductively translated in linear-time into VLTL.

In

*Proc. of the 7th Int'l Joint Conf. on Automated Reasoning (IJCAR'14)*, vol 8562 of LNCS, pp 418-433, Springer, 2014. ISBN 978-3-319-08586-9.