Model-checking in dense real-time (Q689092)

The paper extends model checking for branching-time logic CTL (computation tree logic) to the analysis of real-time systems, whose correctness depends on the magnitudes of the timing delays. For specification, the syntax of CTL is extended to allow quantitative temporal operators. The formulas of the resulting logic, Timed CTL (TCTL) are interpreted over continuous computation trees i.e. trees in which paths are maps from the set of nonnegative reals to system states. Timed graphs are introduced to model finite-state systems. These are state- transition graphs annotated with timing constrains. As the main result, an algorithm for model-checking, for determining the truth of a TCTL- formula with respect to a timed graphs is developed. The algorithm is exponential in the number of clocks and the length of the timing constraints, but linear in the size of the state-transition graph and the length of the formula. It is shown that the problem is PSPACE-complete. It is argued that choosing a dense domain instead of a discrete domain to model time does not significantly blow up the complexity of the model- checking problem. On the other side, it is shown that the denseness of the underlying time domain makes the validity problem for CTL \(\prod^ 1_ 1\)hard. The question of deciding whether there exists a timed graph satisfying a TCTL-formula is also undecidable.