English (United Kingdom)

https://curated-unify.zendy.io/wp-json/zendy-region/v1/featured_content/oa?rat=en

https://curated-unify.zendy.io/wp-json/zendy-region/v1/highlighted_journal/

Global: Zendy Plus annual

Presents the access of premium content as premium feature

Premium Content

Presents the keyphrase highlighting as premium feature

Keyphrase Highlighting

Presents the summarisation as premium feature

Summarisation

Insights

Presents the pdf analysis as premium feature

PDF Analysis

Presents the zaia usage as premium feature

ZAIA

Global: Zendy Plus monthly

Global: Zendy Tools annual

Global: Zendy Tools monthly

Global: Zendy Free Plan

The paper is focused on temporal logics for the description of the behaviourof real-time pushdown reactive systems. The paper is motivated to bridgetractable logics specialized for expressing separately dense-time real-timeproperties and context-free properties by ensuring decidability andtractability in the combined setting. To this end we introduce two real-timelinear temporal logics for specifying quantitative timing context-freerequirements in a pointwise semantics setting: Event-Clock Nested TemporalLogic (ECNTL) and Nested Metric Temporal Logic (NMTL). The logic ECNTL is anextension of both the logic CARET (a context-free extension of standard LTL)and Event-Clock Temporal Logic (a tractable real-time logical framework relatedto the class of Event-Clock automata). We prove that satisfiability of ECNTLand visibly model-checking of Visibly Pushdown Timed Automata VPTA againstECNTL are decidable and EXPTIME-complete. The other proposed logic NMTL is acontext-free extension of standard Metric Temporal Logic (MTL). It is wellknown that satisfiability of future MTL is undecidable when interpreted overinfinite timed words but decidable over finite timed words. On the other hand,we show that by augmenting future MTL with future context-free temporaloperators, the satisfiability problem turns out to be undecidable also forfinite timed words. On the positive side, we devise a meaningful and decidablefragment of the logic NMTL which is expressively equivalent to ECNTL and forwhich satisfiability and visibly model-checking of VPTA are EXPTIME-complete.

Timed context-free temporal logics (extended version)