On liveness and boundedness of asymmetric choice nets
β Scribed by Li Jiao; To-Yat Cheung; Weiming Lu
- Book ID
- 104325903
- Publisher
- Elsevier Science
- Year
- 2004
- Tongue
- English
- Weight
- 444 KB
- Volume
- 311
- Category
- Article
- ISSN
- 0304-3975
No coin nor oath required. For personal study only.
β¦ Synopsis
This paper concerns two important techniques, characterization and property-preserving transformation, for verifying some basic properties of asymmetric choice Petri nets (AC nets). In the literature, a majority of the characterizations are for ordinary free choice nets. This paper presents many extended (from free choice nets) and new characterizations for four properties: liveness with respect to an initial marking, liveness monotonicity with respect to an initial marking, well-formedness, liveness and boundedness with respect to an initial marking. The nets involved are extended to homogeneous free choice nets, ordinary AC nets and homogeneous AC nets. This paper also investigates the transformation of merging a set of places of an ordinary AC net and proposes the conditions for it to preserve the siphon-trap-property (ST-property), liveness, boundedness and reversibility. The results are then applied to the veriΓΏcation of resource-sharing systems. At present, the major approaches for solving this problem are based on state machines or marked graphs and are not based on property preservation. Our approach extends the scopes of the underlying nets to AC nets and the veriΓΏcation techniques. It is found that the ST-property plays a very important role in many of the results. Furthermore, mainly through examples, the importance of the assumptions in the proposed characterizations and transformation and the limitation on further extensions are pointed out.
π SIMILAR VOLUMES
A Petri net (PN) (Pe::erson, 1981;Reisig, 1985) is said to be live if it is possible to fire any transition from every reachable marking, although not: necessarily immediately. A free-choice Petri net (FCPN) is a PN, where every arc from a place to a transition is either t~e unique output arc from t