Context-free timed formalisms: Robust automata and linear temporal logics

The paper focuses on automata and linear temporal logics for real-time pushdown reactive systems bridging tractable formalisms specialized for expressing separately dense-time real-time properties and context-free properties though preserving tractability. As for automata, we introduce Event-Clock Nested Automata ( ECNA ), a formalism that combines Event Clock Automata ( ECA ) and Visibly Pushdown Automata ( VPA ). ECNA enjoy the same closure and decidability properties of ECA and VPA expressively extending any previous attempt of combining ECA and VPA . As for temporal logics, we introduce two formalisms for specifying quantitative timing context-free requirements: Event-Clock Nested Temporal Logic ( EC_NTL ) and Nested Metric Temporal Logic ( NMTL ). EC_NTL is an extension of both the logic CaRet and Event-Clock Temporal Logic having Exptime -complete satisfiability of EC_NTL and visibly model-checking of Visibly Pushdown Timed Systems ( VPTS ) against EC_NTL . NMTL is a context-free extension of standard Metric Temporal Logic ( MTL ) which is in general undecidable having, though, a fragment expressively equivalent to EC_NTL with Exptime -complete satisfiability and visibly model-checking of VPTS problems.