Summary: In this paper, to model check real-time value-passing systems, a formal language timed symbolic transition graph and a logic system named timed predicate $μ$-calculus are proposed. An algorithm is presented which is local in that it generates and investigates the reachable state space in top-down fashion and maintains the partition for time evaluations as coarse as possible while on-the-fly instantiating data variables. It can deal with not only data variables with finite value domain, but also the so-called data independent variables with infinite value domain. To authors knowledge, this is the first algorithm for model checking timed systems containing value-passing features.