Supporting symbolic verification in concurrent engineering

In this paper, we consider the problem of symbolic verification of concurrent activities. We define a new representation extending the well known Binary Decision Diagrams (BDDs) [Bry86] to support symbolic verification in Concurrent engineering. Our technique is called IDDs (Interval Decision Diagrams). The techniques of boolean function manipulation, defined on numerical variables using the BDDs, are confronted with a size explosion of the BDDs which represent these functions. This problem is due to the binary encoding of these variables. The construction of these activities requires the introduction of the numerical variables having rather large domains. These large domains make the BDDs inefficient. The IDDs is designed to solve such a constraint. We also present a set of manipulation algorithms, and show the advantages the IDDs with respect to BDDS.