Rights / licenseIn Copyright - Non-Commercial Use Permitted
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. Show more
Journal / seriesTIK Report
PublisherETH Zurich, Computer Engineering and Networks Laboratory
Organisational unit02640 - Inst. f. Technische Informatik und Komm. / Computer Eng. and Networks Lab.
MoreShow all metadata