@article{BOZZELLI2020104673,
    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.},
    Author = {Bozzelli, Laura and Murano, Aniello and Peron, Adriano},
    ISSN = {0890-5401},
    Journal = {Information and Computation},
    Keywords = {Timed Automata, Temporal Logic, Metric Temporal Logic, Model Checking},
    Pages = {104673},
    Title = {Context-Free Timed Formalisms: Robust Automata and Linear Temporal Logics},
    URL = {http://www.sciencedirect.com/science/article/pii/S0890540120301668},
    Year = {2020},
    bdsk-url-1 = {http://www.sciencedirect.com/science/article/pii/S0890540120301668},
    bdsk-url-2 = {https://doi.org/10.1016/j.ic.2020.104673},
    date-added = {2020-12-27 18:38:48 +0100},
    date-modified = {2020-12-27 18:38:48 +0100},
    doi = {10.1016/j.ic.2020.104673}
}

@article{BOZZELLI2020104673, 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.}, Author = {Bozzelli, Laura and Murano, Aniello and Peron, Adriano}, ISSN = {0890-5401}, Journal = {Information and Computation}, Keywords = {Timed Automata, Temporal Logic, Metric Temporal Logic, Model Checking}, Pages = {104673}, Title = {Context-Free Timed Formalisms: Robust Automata and Linear Temporal Logics}, URL = {http://www.sciencedirect.com/science/article/pii/S0890540120301668}, Year = {2020}, bdsk-url-1 = {http://www.sciencedirect.com/science/article/pii/S0890540120301668}, bdsk-url-2 = {https://doi.org/10.1016/j.ic.2020.104673}, date-added = {2020-12-27 18:38:48 +0100}, date-modified = {2020-12-27 18:38:48 +0100}, doi = {10.1016/j.ic.2020.104673} }