Symbolic model checking using interval diagram techniques
Karsten Strehl, Lothar Thiele · Repository for Publications and Research Data (ETH Zurich) · 1998
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 n o vel approach t o s y m bolic model checking of Petri nets and process networks is presented.Several drawbacks of traditional strategies are avoided using IDDs and IMDs.Especially the resulting transition relation IMD is very compact, allowing for fast image computations.Furthermore, no articial limitations concerning place capacities or equivalent have to beintroduced.Additionally, applications concerning scheduling of process networks are feasible.IDDs and IMDs are dened, their properties are described, and computation methods and techniques are given.