Name
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 |
Year | DOI | Venue |
|---|---|---|
1999 | 10.1109/DATE.1999.761216 | Munich |
Keywords | Field | DocType |
Boolean functions,Petri nets,binary decision diagrams,state-space methods,symbol manipulation,Petri nets,binary decision diagrams,image computation technique,implicit construction,interval decision diagram,interval mapping diagrams,multi-valued functions,state explosion problem,state space,symbolic model checking | Petri net,Model checking,Computer science,Algorithm,Binary decision diagram,Theoretical computer science,Model of computation,Influence diagram,State space,Symbolic trajectory evaluation,Formal verification | Conference |
ISBN | Citations | PageRank |
0-7695-0078-1 | 9 | 0.68 |
References | Authors | |
5 | 2 | |
Name | Order | Citations | PageRank |
|---|---|---|---|
| Karsten Strehl | 1 | 134 | 10.86 |
| Lothar Thiele | 2 | 14025 | 957.82 |