1,721,091 research outputs found
Constraining Cycle Alternations in Model Checking for Interval Temporal Logic
Full text linkModel checking is one of the most successful techniques in system verification. While a variety of methods and tools exist to check properties expressed in point-based temporal logics, like LTL and CTL, model checking for interval temporal logic has entered the research agenda only very recently. In previous work, we devised a non-elementary model checking procedure for Halpern and Shoham's modal logic of time intervals, interpreted over finite Kripke structures, and an EXPSPACE algorithm for two meaningful fragments of it. In this paper, we show that the latter algorithm can be suitably tailored in order to check a subset of the computations of a system, that satisfy a given bound on the number of cycle alternations, by making use of a polynomial (instead of exponential) working space. We also prove that such a revised algorithm turns out to be complete for Kripke structures whose strongly connected components are simple cycle
Timed recursive state machines: Expressiveness and complexity
No full textThe paper proposes a temporal extension of Recursive State Machines (RSMs), called Timed RSMs (TRSMs), which consists of an indexed collection of Timed Automata, called components. Each component can invoke other components in a potentially recursive manner. Besides being able to model procedure calls and recursion, TRSMs are equipped with the ability to suspend the evolution of time within a component when another component is invoked and to recover it when control is given back at return time. This mechanism is realized by storing clock valuations into an implicit stack at invocation time and restoring them upon return. Indeed, TRSMs can be related to an extension of Pushdown Timed Automata, called EPTAs, where an additional stack, coupled with the standard control stack, is used to store temporal valuations of clocks. The expressiveness and computational properties of the resulting model are analyzed, showing that it can be used to recognize timed languages exhibiting context-free properties not only in the untimed “control” part, but also in the associated temporal dimension. The reachability problem for both TRSMs and EPTAs is investigated, showing that the problem is undecidable in the general case. However, the problem becomes decidable for two meaningful subclasses, called I-TRSM and L-TRSM, obtained by suitably constraining the set of clocks to reset at invocation time and to restore at return time. The considered subclasses are compared with the corresponding EPTAs subclasses through bisimulation of their timed LTSs. The complexity of the reachability problem for L-TRSM and I-TRSM is proved to be EXPTIME-complete and PSPACE-complete, respectively. Moreover, we prove that such classes strictly enhance the expressive power of Timed Automata and of Pushdown Timed Automata, forming a proper hierarchy
Timed context-free temporal logics
Full text linkThe 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-complet
Retiming techniques for Statechatrs
No full textWe consider a version of Statecharts having transitions with durations. We relate occurrences of transitions with a dense time domain and enforce a strong time semantics. We examine how durations associated with transitions can be changed while preserving behaviour (a retiming). We discuss also how a class of changes of the temporal feature of the environment (i.e. from non-discrete to discrete and vice-versa, shift, speed-up and slow-down) affect behaviour
The taming (timing) of the states
No full textLogic and computer science communities have traditionally followed a different approach to the problem of representing and reasoning about time and states. Research in logic resulted in a family of (metric) tense logics that take time as a primitive notion and definite (timed) states as sets of atomic propositions which are true at given instants, while research in computer science concentrated on the so-called (real-time) temporal logics of programs that take state as a primitive notion, and define time as an attribute of states. In this paper, we provide a unifying framework within which the two approaches can be reconciled. Our main tools are metric and layered temporal logics originally proposed to model time granularity in various contexts. In such a framework, states and time-instants can be uniformly referred to as elements of a (decidable) theory of omega-layered metric temporal structures. Furthermore, we show that the theory of timed state sequences, underlying real-time logics, is naturally recovered as an abstraction of such a theory
- …
