Minimum and maximum delay problems in real-time systems
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\).
- Robust safety of timed automata
- The power of reachability testing for timed automata
- On a class of timer hybrid systems reducible to finite state automata
- Is your model checker on time? On the complexity of model checking for timed modal logics
- Reachability in two-clock timed automata is PSPACE-complete
- Scheduling with timed automata
- Efficient timed model checking for discrete-time systems
- Schedulability of asynchronous real-time concurrent objects
- Model checking restricted sets of timed paths
- Model-based verification, optimization, synthesis and performance evaluation of real-time systems
- Fair termination for parameterized probabilistic concurrent systems
- Concavely-Priced Timed Automata
- A survey of timed automata for the development of real-time systems
- Interrupt timed automata: verification and expressiveness
- Minimum Deadline Calculation for Periodic Real-Time Tasks in Dynamic Priority Systems
- Parametric metric interval temporal logic
- Finding minimum and maximum termination time of timed automata models with cyclic behaviour
- Compositional schedulability analysis of real-time actor-based systems
- A performance analysis of minimum laxity and earliest deadline scheduling in a real-time system
- An introduction to timed automata
- Reachability for bounded branching VASS
- Verifying time Petri nets by linear programming
- Optimal paths in weighted timed automata
- On the minimum delay problem
- Checking timed Büchi automata emptiness efficiently
- Folk theorems on the determinization and minimization of timed automata
This page was built for publication: Minimum and maximum delay problems in real-time systems
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q685111)
