DocumentCode
2844328
Title
Calculating place capacity for Petri nets using unfoldings
Author
Miyamoto, T. ; Kumagai, S.
Author_Institution
Dept. of Electr. Eng., Osaka Univ., Japan
fYear
1998
fDate
23-26 Mar 1998
Firstpage
143
Lastpage
151
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;
fLanguage
English
Publisher
ieee
Conference_Titel
Application of Concurrency to System Design, 1998. Proceedings., 1998 International Conference on
Conference_Location
Fukushima
Print_ISBN
0-8186-8350-3
Type
conf
DOI
10.1109/CSD.1998.657547
Filename
657547
Link To Document