 |
|
|||
| Authors: | Karsten Strehl, Lothar Thiele |
| Group: | Computer Engineering |
| Type: | Inproceedings |
| Title: | Interval Diagram Techniques for Symbolic Model Checking of Petri Nets |
| Year: | 1999 |
| Month: | March |
| Pub-Key: | ST99a |
| Book Titel: | Proceedings of the Design, Automation and Test in Europe Conference (DATE99) |
| Pages: | 756-757 |
| Keywords: | SMC IDD |
| Abstract: | Symbolic model checking tries to reduce the state explosion problem by implicit construction of the state space. The major limiting factor is the size of the symbolic representation mostly stored in huge binary decision diagrams. A new approach to symbolic model checking of Petri nets and related models of computation is presented, outperforming the conventional one and avoiding some of its drawbacks. Our approach is based on a novel, efficient form of representation for multi-valued functions called interval decision diagram (IDD) and the corresponding image computation technique using interval mapping diagrams (IMDs). IDDs and IMDs are introduced, their properties are described, and the feasibility of the new approach is shown with some experimental results. |
| Remarks: | Proceedings of the Design, Automation and Test in Europe Conference (DATE99), pages 756-757, Munich, Germany, March 9-12, 1999 |
| Location: | Munich, Germany |
| Resources: | [BibTeX] [Paper as PDF] |
