In this paper, we develop a symbolic representation for timed concurrent constraint (tccp)
programs, which can be used for defining a new model-checking algorithm
for reactive systems. Our approach is based on using streams to extend Difference Decision Diagrams (DDDs)
which generalize the classical Binary
Decision Diagrams (BDDs) with constraints. We use streams to
model the values of system variables along the time, as occurs in many
other (declarative) languages. Then, we define a symbolic (finite
states) model checking algorithm for tccp which mitigates the state
explosion problem that is common to more conventional model-checking
approaches. In particular, we show how the symbolic approach to model
checking for tccp improves
previous approaches based on the classical Linear Time Logic (LTL)
model checking algorithm.
Keywords: Timed Concurrent
Constraint Programming, Model Checking, DDDs