Title :
Calculating place capacity for Petri nets using unfoldings
Author :
Miyamoto, T. ; Kumagai, S.
Author_Institution :
Dept. of Electr. Eng., Osaka Univ., Japan
Abstract :
Though Petri nets have powerful mathematical verification ability, we have to construct the state space in many cases. An upper bound of a place is the maximum number of tokens on the place for all reachable markings. We can find the upper bound by using a reachability graph or S-invariants. This paper proposes a method to find the upper bound by using an unfolding, and a comparison is made among these methods
Keywords :
Petri nets; formal verification; reachability analysis; Petri nets; S-invariants; mathematical verification; place capacity calculation; reachability graph; reachable markings; state space; unfoldings; upper bound; Asynchronous circuits; Binary decision diagrams; Character recognition; Discrete event systems; Equations; Flexible manufacturing systems; Matrix decomposition; Petri nets; Power system modeling; Upper bound;
Conference_Titel :
Application of Concurrency to System Design, 1998. Proceedings., 1998 International Conference on
Conference_Location :
Fukushima
Print_ISBN :
0-8186-8350-3
DOI :
10.1109/CSD.1998.657547
