ﻻ يوجد ملخص باللغة العربية
The paper is focused on temporal logics for the description of the behaviour of real-time pushdown reactive systems. The paper is motivated to bridge tractable logics specialized for expressing separately dense-time real-time properties and context-free properties by ensuring decidability and tractability in the combined setting. To this end we introduce two real-time linear temporal logics for specifying quantitative timing context-free requirements in a pointwise semantics setting: Event-Clock Nested Temporal Logic (EC_NTL) and Nested Metric Temporal Logic (NMTL). The logic EC_NTL is an extension of both the logic CaRet (a context-free extension of standard LTL) and Event-Clock Temporal Logic (a tractable real-time logical framework related to the class of Event-Clock automata). We prove that satisfiability of EC_NTL and visibly model-checking of Visibly Pushdown Timed Automata (VPTA) against EC_NTL are decidable and EXPTIME-complete. The other proposed logic NMTL is a context-free extension of standard Metric Temporal Logic (MTL). It is well known that satisfiability of future MTL is undecidable when interpreted over infinite timed words but decidable over finite timed words. On the other hand, we show that by augmenting future MTL with future context-free temporal operators, the satisfiability problem turns out to be undecidable also for finite timed words. 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 VPTA are EXPTIME-complete.
The paper is focused on temporal logics for the description of the behaviour of real-time pushdown reactive systems. The paper is motivated to bridge tractable logics specialized for expressing separately dense-time real-time properties and context-f
In temporal logics, a central question is about the choice of modalities and their relative expressive power, in comparison to the complexity of decision problems such as satisfiability. In this tutorial, we will illustrate the study of such question
The problem of model checking procedural programs has fostered much research towards the definition of temporal logics for reasoning on context-free structures. The most notable of such results are temporal logics on Nested Words, such as CaRet and N
Nested words are a structured model of execution paths in procedural programs, reflecting their call and return nesting structure. Finite nested words also capture the structure of parse trees and other tree-structured data, such as XML. We provide n
We prove that the determinacy of Gale-Stewart games whose winning sets are accepted by real-time 1-counter Buchi automata is equivalent to the determinacy of (effective) analytic Gale-Stewart games which is known to be a large cardinal assumption. We