As the complexity of software systems increases, automatic verification tools which are able to guarantee the correct behavior of such systems are dramatically lacking. Model checking is a formal verification technique which allows one to automatically check whether a specific property is satisfied by a model of the system; otherwise it provides a counterexample which helps the programmer to debug the wrong code.
 
In this paper we develop a symbolic model checking technique for the Timed Concurrent Constraint Language (tccp), a declarative language within the concurrent constraint paradigm which allows one to program reactive systems in a very natural way. Two of the most important features of the language are the use of constraints and a notion of time which is within the operational model. By taking advantage of these two features and using an extension of Difference Decision Diagrams (DDDs), we formulate a symbolic model checking algorithm for tccp which mitigates the state explosion problem that is common to model checking approaches. The symbolic approach to model checking tccp leads to an important improvement w.r.t. previous approaches based on the classical Linear Time Logic (LTL) model checking algorithm.