Return to search

應用同步選擇網路在派翠網路之分析 / Application of SNC (Synchronized choice net) to analysis Petri nets

Well-behaved SNC covers well-behaved and various classes of FC (free-choice) and is not included in AC (asymmetric choice). An SNC allows internal choices and concurrency and hence is powerful for irodeling. Any SNC is bounded and its liveness conditions are simple. An integrated algorithm, has been presented for verification of a net being SNC and its liveness with polynomial time complexity. Scholars often need to verify properties on nets appearing in literatures. Verification by CAD tool is less desirable than that by hand due to the extra efforts to input the model aid learn to use the tool. We propose to manually search the maximum SNC component followed by locating bad siphons in an incremental manner. We then apply Lautenback's Maridng Condition (MC) for liveness to berify the property of liveness. But there are two drawbacks associated with the above MC. First, it guarantees only deadlock-freeness, and not necessary liveness. We have identified the structure cause for this and developed its livess conditions correspondingly. Second a net may be live even if the MC is not satisfied. We have identified the structure cause for this. The MC has been readjusted based on our proposed new theorey.

Identiferoai:union.ndltd.org:CHENGCHI/A2002001611
Creators巫亮宏
Publisher國立政治大學
Source SetsNational Chengchi University Libraries
Language英文
Detected LanguageEnglish
Typetext
RightsCopyright © nccu library on behalf of the copyright holders

Page generated in 0.0016 seconds