Typical questions to be answered by formal verification of process networks are about the absence of deadlocks, the boundedness of the required memory, or proving certain properties of the specification. Especially memory boundedness is important as process networks in general may not be scheduled statically. Thus, dynamic schedulers have to be deployed which cannot always guarantee to comply with memory limitations. Formal verification may assist during development of scheduling strategies by confirming the compliance with explicit resource limitations or by determining inherent bounds.

During the last years, a promising approach named symbolic model checking was applied to many areas of system verification in computer engineering and related research fields and even has been able to enter the area of industrial applications. It makes use of binary decision diagrams (BDDs) which are an efficient representation of Boolean functions and allow for their very fast manipulation. But when applying this technique to process networks or related models of computation, several difficulties occur that question its usefulness in this area. The major limiting factor of symbolic model checking is the state explosion problem caused by the queues of potentially unlimited length.

To overcome several limitations of conventional symbolic model checking of process networks, we present an approach that uses interval decision diagrams (IDDs) combined with interval mapping diagrams (IMDs) – especially their restricted form predicate action diagrams (PADs) – and thus is able to remedy described lacks of traditional approaches. Fundamentally, it is based on a more reasonable way of describing the mentioned form of transition relations. Major enhancements of symbolic model checking with IDDs and IMDs are:

• No restrictions on the model are necessary as with conventional symbolic model checking.
• The transition relation representation is quite compact – especially for process networks. The innovative technique for efficient image computation outperforms the conventional one.
• Due to the enhanced merging capabilities of IDDs, state set descriptions are more compact than using BDDs, reducing the state explosion problem.