 |
|
|||
| Authors: | Karsten Strehl, Lothar Thiele |
| Group: | Computer Engineering |
| Type: | Techreport |
| Title: | Symbolic Model Checking Using Interval Diagram Techniques |
| Year: | 1998 |
| Month: | February |
| Pub-Key: | ST98a |
| Keywords: | SMC IDD |
| Rep Nbr: | 40 |
| Institution: | Computer Engineering and Networks Lab (TIK), Swiss Federal Institute of Technology (ETH) Zurich |
| 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. |
| Remarks: | TIK Report No. 40, February 1998 |
| Resources: | [BibTeX] [Paper as PDF] |
