Minimum and maximum delay problems in real-time systems (Q685111)

Correctness of real-time systems is more subtle and harder than for traditional systems. One reason for this is that the parameter time is not discrete, does not range over a finite domain, and has its own dynamics beyond the control of the programs. This makes the verification of such systems a challenging and sometimes impossible task. Our model of a real-time system is a timed graph. These graphs model ``finite-state'' real-time systems. Such a system has a finite set of states and a finite set of real-valued clocks. A clock can be reset simultaneously with any transition of the system. At any instant, the value of a clock is equal to the time elapsed since the last time this clock was reset. The real- time information is given in terms of enabling conditions of the edges; a transition is enabled if the values of the clocks satisfy a certain predicate. The semantics of such graphs is the following. The system starts in some initial state \(s_ 0\) with some initial clock assignment. The values of the clocks increase uniformly with time. At any point in time, the system can make a transition if the associated condition is enabled by the current values of the clocks. The transitions are instantaneous. With each transition the clocks that must be reset get reset to 0 and start counting time with respect to the time the transition occurred. At any point in time, the complete configuration of the system is described by specifying the current state and the values of the clocks. Clearly, such a system has uncountably many configurations. We examine the complexity of the following problems in the context of timed graphs. Given a timed graph \({\mathcal G}\), some initial state \(s_ 0\), some initial clock assignment \(v\), and some final state \(s_ f\), (a) (The Timed Graph reachability Problem) determine if \(s_ f\) appears in some real-time trajectory of \(G\) starting from configuration \((s_ 0,v)\); (b) (The Minimum Delay Problem in Timed Graphs) how fast can we reach \(s_ f\) starting from the configuration \((s_ 0,v)\); (c) (The Maximum Delay Problem in timed graphs) find the least upper bound on the time \(t\) at which any real-time trajectory of the system visits a configuration with state \(s_ f\). In both the maximum and the minimum delay problems we are also interested in the variants where we are not given an initial clock assignment \(v\), but rather we wish to optimize over all possible \(v\).