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

In a previous paper we introduced immediate observation (IO) Petri nets, aclass of interest in the study of population protocols and enzymatic chemicalnetworks. In the first part of this paper we show that IO nets are globallyflat, and so their safety properties can be checked by efficient symbolic modelchecking tools using acceleration techniques, like FAST. In the second part westudy Branching IO nets (BIO nets), whose transitions can create tokens. BIOnets extend both IO nets and communication-free nets, also called BPP nets, awidely studied class. We show that, while BIO nets are no longer globally flat,and their sets of reachable markings may be non-semilinear, they are stilllocally flat. As a consequence, the coverability and reachability problem forBIO nets, and even a certain set-parameterized version of them, are in PSPACE.This makes BIO nets the first natural net class with non-semilinearreachability relation for which the reachability problem is provably simplerthan for general Petri nets.

Flatness and Complexity of Immediate Observation Petri Nets