{
  "id": "2103.02475",
  "version": "v1",
  "published": "2021-03-03T15:37:05.000Z",
  "updated": "2021-03-03T15:37:05.000Z",
  "title": "Non-Blockingness Verification of Bounded Petri Nets Using Basis Reachability Graphs",
  "authors": [
    "Chao Gu",
    "Ziyue Ma",
    "Zhiwu Li",
    "Alessandro Giua"
  ],
  "categories": [
    "eess.SY",
    "cs.SY"
  ],
  "abstract": "In this paper, we study the problem of non-blockingness verification by tapping into the basis reachability graph (BRG). Non-blockingness is a property that ensures that all pre-specified tasks can be completed, which is a mandatory requirement during the system design stage. In this paper we develop a condition of transition partition of a given net such that the corresponding conflict-increase BRG contains sufficient information on verifying non-blockingness of its corresponding Petri net. Thanks to the compactness of the BRG, our approach possesses practical efficiency since the exhaustive enumeration of the state space can be avoided. In particular, our method does not require that the net is deadlock-free.",
  "revisions": [
    {
      "version": "v1",
      "updated": "2021-03-03T15:37:05.000Z"
    }
  ],
  "analyses": {
    "keywords": [
      "basis reachability graph",
      "bounded petri nets",
      "non-blockingness verification",
      "conflict-increase brg contains sufficient information",
      "corresponding conflict-increase brg contains sufficient"
    ],
    "note": {
      "typesetting": "TeX",
      "pages": 0,
      "language": "en",
      "license": "arXiv",
      "status": "editable"
    }
  }
}