Analysis of Behavioural Properties of Bounded Petri Nets with a Semi-Structural Approach
Gu C.First
;Giua A.Last
2020-01-01
Abstract
In this paper, we propose a semi-structural approach to verify some behavioural properties of bounded Petri nets, including home state existence, reversibility, liveness, and deadlock-freeness. An abstracted representation of the state space of Petri nets, called minimax basis reachability graph (minimax-BRG), is employed. We show how the verification of the above-mentioned properties for a bounded Petri net can be carried out testing equivalent properties of its corresponding minimax-BRG. Being the minimax-BRGs an abstracted representation of the reachability graph, the exhaustive enumeration of the state space can be avoided and we show, via numerical simulations, that this approach achieves significant practical efficiency.File | Size | Format | |
---|---|---|---|
20cdc_a.pdf Solo gestori archivio
Type: versione editoriale
Size 444.47 kB
Format Adobe PDF
|
444.47 kB | Adobe PDF | & nbsp; View / Open Request a copy |
Items in DSpace are protected by copyright, with all rights reserved, unless otherwise indicated.