Linear temporal logics for structured context-free languages

The need to extend traditional temporal logics to express and prove properties typical of stack-based formalisms led, among others, to CaRet and NWTL on Visibly Pushdown Languages (VPL). Such formalisms support, e.g., model checking of procedural programs and other context-free languages (CFL). To further and significantly extend their expressive power, we recently introduced the logic OPTL, based on Operator Precedence Languages (OPL) which cover a much wider subclass of CFL. In this communication we survey the latest developments of our work. We introduced a novel temporal logic, POTL, that redefines OPTL to be First-Order complete. Furthermore, POTL's semantics is better connected to the typical tree-structure of CFL while retaining the ability to reason about linear time. Besides the theoretical advancements, we are also moving steps toward the implementation of POTL model checking.