For the most recent entries see the Petri Nets Newsletter.

Interval Diagram Techniques for Symbolic Model Checking of Petri Nets.

Strehl, Karsten; Thiele, Lothar

In: Proceedings of the Design, Automation and Test in Europe Conference (DATE'99), Munich, Germany, March 9-12, 1999, pages 756-757. 1999.

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: Symbolic model checking, reachability analysis, binary decision diagrams, interval diagram techniques.


Do you need a refined search? Try our search engine which allows complex field-based queries.

Back to the Petri Nets Bibliography