Minimum and maximum delay problems in real-time systems.

*(English)*Zbl 0777.68045Correctness 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\).

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\).

Reviewer: C.Courboubetis

##### MSC:

68Q25 | Analysis of algorithms and problem complexity |

68R10 | Graph theory (including graph drawing) in computer science |

68Q60 | Specification and verification (program logics, model checking, etc.) |

##### Keywords:

finite state system; times; shortest path; reachability problem; correctness of real-time systems; timed graphs; delay problems
PDF
BibTeX
XML
Cite

\textit{C. Courcoubetis} and \textit{M. Yannakakis}, Form. Methods Syst. Des. 1, No. 4, 385--415 (1992; Zbl 0777.68045)

Full Text:
DOI

##### References:

[1] | S.Aggarwal and R.Kurshan, Modeling elapsed time in protocol specification,Proc. Protocol Specification, Testing and Verification, 3: 51-62, 1983. |

[2] | R. Alur, C. Courcoubetis, and D. Dill. Model-checking for real-time systems.Proc. 5th IEEE Symposium on Logic in Computer Science, pp. 414-425, 1990. · Zbl 0769.68088 |

[3] | R.Alur and D.Dill. Automata for modeling real-time systems.Proc. 17th International Collaboration on Automata, Languages and Programming. Lecture Notes in Computer Science, 443: 322-335, 1990. · Zbl 0765.68150 |

[4] | R. Alur and T. Henzinger. A really temporal logic.Proc. 30th Annual IEEE Symposium on Foundations of Computer Science, pp. 164-169, 1989. · Zbl 0807.68065 |

[5] | D. Dill. Timing assumptions and verification of finite-state concurrent systems.Automatic Verification Methods for Finite-State Systems. Lecture Notes in Computer Science, 407:,1989. |

[6] | H. Lewis, A logic of concrete time intervals.Proc. 5th IEEE Symp. on Logic in Computer Science, pp. 380-389, 1990. |

[7] | R. Alur, C. Courcoubetis, and D. Dill. Probabilistic model checking of real-time systems.Proc. 18th International Collaboration on Automata, Languages and Programming. Lecture Notes in Computer Science, 510: 1991. · Zbl 0769.68088 |

[8] | T.H.Corman, C.E.Leiserson, and R.L.Rivest.Introduction to Algorithms, McGraw Hill, New York, 1990. |

[9] | M. Fredman and R.E. Tarjan. Fibonacci heaps and their uses in improved network. |

This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. It attempts to reflect the references listed in the original paper as accurately as possible without claiming the completeness or perfect precision of the matching.