Interval diagram techniques for symbolic model checking of Petri nets
- 20 January 2003
- conference paper
- Published by Institute of Electrical and Electronics Engineers (IEEE)
- p. 756-757
- https://doi.org/10.1109/date.1999.761216
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.Keywords
This publication has 3 references indexed in Scilit:
- Symbolic model checking: 1020 States and beyondPublished by Elsevier ,2004
- Algorithms for discrete function manipulationPublished by Institute of Electrical and Electronics Engineers (IEEE) ,2002
- Graph-Based Algorithms for Boolean Function ManipulationIEEE Transactions on Computers, 1986