Verification of Nonblockingness in Bounded Petri Nets With Minimax Basis Reachability Graphs
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.
Code (0)
등록된 구현이 없습니다.
Tasks
BlockingSimilar Papers 제목 키워드 기반
Verification of Detectability Using Petri Nets and Detector
Detectability describes the property of a system to uniquely determine, after a finite number of observations, the current and subsequent states. In this paper, to reduce the complexity of checking the detectability prop…
Non-Blockingness Verification of Bounded Petri Nets Using Basis Reachability Graphs -- An Extended Version With Benchmarks
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…
Bounded-Time Nonblocking Supervisory Control of Timed Discrete-Event Systems
Recently an automaton property of quantitative nonblockingness was proposed in supervisory control of untimed discrete-event systems (DES), which quantifies the standard nonblocking property by capturing the practical re…
Simulating Petri nets with Boolean Matrix Logic Programming
Recent attention to relational knowledge bases has sparked a demand for understanding how relations change between entities. Petri nets can represent knowledge structure and dynamically simulate interactions between enti…
Acyclic and Cyclic Reversing Computations in Petri Nets
Reversible computations constitute an unconventional form of computing where any sequence of performed operations can be undone by executing in reverse order at any point during a computation. It has been attracting incr…