Sciweavers

APN
2004
Springer

Reachability Set Generation for Petri Nets: Can Brute Force Be Smart?

14 years 4 months ago
Reachability Set Generation for Petri Nets: Can Brute Force Be Smart?
Generating the reachability set is one of the most commonly required step when analyzing the logical or stochastic behavior of a system modeled with Petri nets. Traditional “explicit” algorithms that explore the reachability graph of a Petri net require memory and time at least proportional to the number of reachable markings, thus they are applicable only to fairly small systems in practice. Symbolic “implicit” algorithms, typically implemented using binary decision diagrams, have been successfully employed in much larger systems, but much of the work to date is based on breadth-first search techniques best suited for synchronous hardware verification. Here, instead, we describe recentlyintroduced data structures and algorithms particularly targeted to Petri nets and similar asynchronous models, and show why they are enormously more efficient for this application. We conclude with some directions for future research.
Gianfranco Ciardo
Added 30 Jun 2010
Updated 30 Jun 2010
Type Conference
Year 2004
Where APN
Authors Gianfranco Ciardo
Comments (0)