Interval diagrams for efficient symbolic verification of process networks

In this paper, a representation of multivalued functions called interval de cision diagrams (IDDs) is introduced. It is related to similar representati ons such as binary decision diagrams. Compared to other functional represen tations with regard to symbolic formal verification approaches, IDDs show s ome important properties that enable us to verify process networks and rela ted models of computation more adequately than with conventional approaches . Therefore, a new form of transition relation representation called interv al mapping diagram (IMD) is introduced. A novel approach to symbolic model checking of process networks is presente d, Several drawbacks of traditional strategies are avoided using IDDs and I MDs. The resulting transition relation IMD is very compact, enabling fast i mage computations. Furthermore, no artificial limitations concerning buffer capacities or equivalent have to be introduced. Additionally, applications concerning scheduling of process networks are feasible. IDDs and IMDs are defined, their properties are described, and computation methods and techni ques are given.