English (United Kingdom)

https://curated-unify.zendy.io/wp-json/zendy-region/v1/featured_content/oa?rat=en

https://curated-unify.zendy.io/wp-json/zendy-region/v1/highlighted_journal/

Global: Zendy Plus annual

Presents the access of premium content as premium feature

Premium Content

Presents the keyphrase highlighting as premium feature

Keyphrase Highlighting

Presents the summarisation as premium feature

Summarisation

Insights

Presents the pdf analysis as premium feature

PDF Analysis

Presents the zaia usage as premium feature

ZAIA

Global: Zendy Plus monthly

Global: Zendy Tools annual

Global: Zendy Tools monthly

Global: Zendy Free Plan

This paper proposes a semi-structural approach to verify the nonblockingnessof a Petri net. We construct a structure, called minimax basis reachabilitygraph (minimax-BRG): it provides an abstract description of the reachabilityset of a net while preserving all information needed to test if the net isblocking. We prove that a bounded deadlock-free Petri net is nonblocking if andonly if its minimax-BRG is unobstructed, which can be verified by solving a setof integer constraints and then examining the minimax-BRG. For Petri nets thatare 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 implicitfiring sequences enabled by the markings in the minimax-BRG. The approach wedeveloped does not require the construction of the reachability graph and haswide applicability.

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