Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

Verification of Nonblockingness in Bounded Petri Nets With Minimax Basis Reachability Graphs

Chao Gu, Ziyue Ma, Zhiwu Li, Alessandro Giua

TL;DR

It is proved that a bounded deadlock-free Petri net is nonblocking if and only if its min-max-BRG is unobstructed, which can be verified by solving a set of integer constraints and then examining the min- Max BRG.

Abstract

This paper proposes a semi-structural approach to verify the nonblockingness of a Petri net. We construct a structure, called minimax basis reachability graph (minimax-BRG): it provides an abstract description of the reachability set of a net while preserving all information needed to test if the net is blocking. We prove that a bounded deadlock-free Petri net is nonblocking if and only if its minimax-BRG is unobstructed, which can be verified by solving a set of integer constraints and then examining the minimax-BRG. For Petri nets that are not deadlock-free, one needs to determine the set of deadlock markings. This can be done with an approach based on the computation of maximal implicit firing sequences enabled by the markings in the minimax-BRG. The approach we developed does not require the construction of the reachability graph and has wide applicability.

Verification of Nonblockingness in Bounded Petri Nets With Minimax Basis Reachability Graphs

TL;DR

It is proved that a bounded deadlock-free Petri net is nonblocking if and only if its min-max-BRG is unobstructed, which can be verified by solving a set of integer constraints and then examining the min- Max BRG.

Abstract

This paper proposes a semi-structural approach to verify the nonblockingness of a Petri net. We construct a structure, called minimax basis reachability graph (minimax-BRG): it provides an abstract description of the reachability set of a net while preserving all information needed to test if the net is blocking. We prove that a bounded deadlock-free Petri net is nonblocking if and only if its minimax-BRG is unobstructed, which can be verified by solving a set of integer constraints and then examining the minimax-BRG. For Petri nets that are not deadlock-free, one needs to determine the set of deadlock markings. This can be done with an approach based on the computation of maximal implicit firing sequences enabled by the markings in the minimax-BRG. The approach we developed does not require the construction of the reachability graph and has wide applicability.

Paper Structure

This paper contains 15 sections, 11 theorems, 5 equations, 4 figures, 1 table, 2 algorithms.

Table of Contents

  1. Introduction
  2. Preliminaries
  3. Automata and Petri nets
  4. Basis Reachability Graph (BRG) c3c8Basis
  5. BRG and Nonblockingness Verification
  6. Minimax Basis Markings and Minimax-BRGs
  7. Minimax Basis Markings
  8. Minimax Basis Reachability Graph
  9. Verifying Nonblockingness of Bounded Plants Using Minimax-BRGs
  10. Unobstructiveness of Minimax-BRGs
  11. Verifying Nonblockingness of Deadlock-Free Plants
  12. Verifying Nonblockingness of Plants with Deadlocks
  13. Case Studyz
  14. Discussions
  15. Conclusions and Future Work

Key Result

Proposition 1

c8Murata Given a marked net $\langle N, M_0\rangle$ where $N$ is acyclic, $M\in R(N, M_0)$, $M^{\prime}\in R(N, M_0)$ and a firing vector $\textbf{y}\in \mathbb{N}^n$, the following holds:

Figures (4)

  • Figure 1: A parameterized plant $G$ with $T_E=\{t_2\}$ marked with shadow (left) and its BRG $\mathcal{B}$ (right).
  • Figure 2: Reachability graph of $G$ in Fig. \ref{['Fig1']} with $\alpha=1$ (left) and $\alpha=2$ (right).
  • Figure 3: The minimax-BRG $\mathcal{B_M}$ with $T_E=\{t_2\}$.
  • Figure 4: A parameterized manufacturing example.

Theorems & Definitions (28)

  • Proposition 1
  • Definition 1
  • Definition 2
  • Definition 3
  • Definition 4
  • Definition 5
  • Definition 6
  • Example 1
  • Definition 7
  • Definition 8
  • ...and 18 more