Abstract The paper is focused on automata and linear temporal logics for describing the behaviour of real-time pushdown reactive systems. The goal of the paper is to bridge (both in the context of automata and linear temporal logics) tractable formalisms specialized for expressing separately dense-time real-time properties and context-free properties though preserving tractability in the combined setting. As for automata, we introduce Event-Clock Nested Automata ( ECNA ), a formalism that combines Event Clock Automata ( ECA ) and Visibly Pushdown Automata ( VPA ). ECNA can express real-time properties over non-regular patterns of timed words. We prove that ECNA enjoy the same closure and decidability properties of ECA and VPA , being closed under Boolean operations and having a decidable language-inclusion problem (indeed emptiness, universality, and language inclusion for ECNA are Exptime -complete). As for expressiveness, ECNA properly extend any previous attempt in the literature of combining ECA and VPA . The results obtained in the automata setting are exploited in the context of linear temporal logics where we introduce two logics 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 (a context-free extension of standard LTL ) and Event-Clock Temporal Logic. We prove that satisfiability of EC_NTL and visibly model-checking of Visibly Pushdown Timed Systems ( VPTS ) against EC_NTL are decidable and Exptime -complete. NMTL is instead a context-free extension of standard Metric Temporal Logic ( MTL ). The interesting result is that by augmenting future MTL with future context-free temporal operators, the satisfiability problem for finite timed words–which is decidable for future MTL – turns out to be undecidable. On the positive side, we devise a meaningful and decidable fragment of the logic NMTL which is expressively equivalent to EC_NTL and for which satisfiability and visibly model-checking of VPTS are Exptime -complete.
Paper
Full text
Context-free timed formalisms: Robust automata and linear temporal logics
Semantic Scholar · Computer Science · 2020
Abstract
Abstract The paper is focused on automata and linear temporal logics for describing the behaviour of real-time pushdown reactive systems. The goal of the paper is to bridge (both in the context of automata and linear temporal logics) tractable formalisms specialized for expressing separately dense-time real-time properties and context-free properties though preserving tractability in the combined setting. As for automata, we introduce Event-Clock Nested Automata ( ECNA ), a formalism that combines Event Clock Automata ( ECA ) and Visibly Pushdown Automata ( VPA ). ECNA can express real-time properties over non-regular patterns of timed words. We prove that ECNA enjoy the same closure and decidability properties of ECA and VPA , being closed under Boolean operations and having a decidable language-inclusion problem (indeed emptiness, universality, and language inclusion for ECNA are Exptime -complete). As for expressiveness, ECNA properly extend any previous attempt in the literature of combining ECA and VPA . The results obtained in the automata setting are exploited in the context of linear temporal logics where we introduce two logics 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 (a context-free extension of standard LTL ) and Event-Clock Temporal Logic. We prove that satisfiability of EC_NTL and visibly model-checking of Visibly Pushdown Timed Systems ( VPTS ) against EC_NTL are decidable and Exptime -complete. NMTL is instead a context-free extension of standard Metric Temporal Logic ( MTL ). The interesting result is that by augmenting future MTL with future context-free temporal operators, the satisfiability problem for finite timed words–which is decidable for future MTL – turns out to be undecidable. On the positive side, we devise a meaningful and decidable fragment of the logic NMTL which is expressively equivalent to EC_NTL and for which satisfiability and visibly model-checking of VPTS are Exptime -complete.