We describe finite-state programs over real-numbered time in a guarded
-command language with real-valued clocks or, equivalently, as finite
automata with real-valued clocks. Model checking answers the question
which states of a real-time program satisfy a branching-time specifica
tion (given in an extension of CTL with clock variables). We develop a
n algorithm that computes this set of states symbolically as a fixpoin
t of a functional on state predicates, without constructing the state
space. For this purpose, we introduce a mu-calculus on computation tre
es over real-numbered time. Unfortunately, many standard program prope
rties, such as response for all nonzeno execution sequences (during wh
ich time diverges), cannot be characterized by fixpoints: we show that
the expressiveness of the timed mu-calculus is incomparable to the ex
pressiveness of timed CTL. Fortunately, this result does not impair th
e symbolic verification of ''implementable'' real-time programs-those
whose safety constraints are machine-closed with respect to diverging
time and whose fairness constraints are restricted to finite upper bou
nds on clock values. All timed CTL properties of such programs are sho
wn to be computable as finitely approximable fixpoints in a simple dec
idable theory. (C) 1994 Academic Press, Inc.