Symbolic model checking using interval diagram techniques

Abstract

In this report, a representation of multi-valued functions called interval decision diagrams (IDDs) is introduced. It is related to similar representations as binary decision diagrams. Compared to other model checking strategies, IDDs show some important properties that enable us to verify especially Petri nets, process networks, and related models of computation more adequately than with conventional approaches. Therefore, a new form of transition relation representation called interval mapping diagrams (IMDs) – and their less general version predicate action diagrams (PADs) – is explained. A novel approach to symbolic model checking of Petri nets and process networks is presented. Several disadvantages arising for traditional strategies are avoided using IDDs and IMDs. Especially the resulting transition relation IMD is very compact, allowing for fast image computations. Furthermore, no artificial limitations concerning place 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 techniques are given.