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

Although decidable, the marking reachability problem for Petri nets iswell-known to be intractable in general, and a non-elementary lower bound hasbeen recently uncovered. In order to alleviate this difficulty, variousstructural and behavioral restrictions have been considered, allowing to relatereachability to properties that are easier to check. For a given initialmarking, the set of potentially reachable markings is described by the stateequation solutions and over-approximates the set of reachable markings.  In this paper, we delineate several subclasses of weighted Petri nets inwhich the set of reachable markings equals the set of potentially reachableones, a property we call the PR-R equality. When fulfilled, this propertyallows to use linear algebra to answer the reachability questions, avoiding abrute-force analysis of the state space. Notably, we provide conditions underwhich this equality holds in classes much more expressive than marked graphs,adding places with several ingoing and outgoing transitions, which allows tomodel real applications with shared buffers. To achieve it, we investigate therelationship between liveness, reversibility, boundedness and potentialreachability in Petri nets. We also show that this equality does not hold inclasses with close modeling capability when the conditions are relaxed.

Checking marking reachability with the state equation in Petri net subclasses