Verification of Immediate Observation Petri Nets

July 6, 2021

Chana Weil-Kennedy


Verification of Immediate Observation Petri Nets

Time:   11:00am
Location:   Zoom3 - https://zoom.us/j/3911012202 (pass: s3)

Petri nets are a popular and well-studied formal model for the representation and verification of parallel processes. The central problem for Petri nets is reachability: given two configurations of a Petri net, does there exist a run from one to the other. This problem is very difficult: it has recently been proven to be Tower-hard (non-elementary). This motivates the study of subclasses in the hopes of having a more reasonable complexity. Some classic syntactic restrictions of Petri nets are BPP nets (Branching Parallel Process), or marked graphs (sometimes called T-systems). We introduce and study a new syntactic restriction: immediate observation Petri nets (or IO nets), motivated by applications to population protocols — a model of distributed computation — and enzymatic chemical networks. In these areas, relevant analysis questions translate into parameterized problems: whether an infinite set of Petri nets with the same underlying net, but different initial markings, satisfy a given property. We study the parameterized reachability, coverability, and liveness problems for IO nets. We show that all three problems are in PSPACE for infinite sets of initial markings defined by counting constraints, a class sufficiently rich for the intended application. We also show that IO nets are globally flat, and so their safety properties can be checked by efficient symbolic model checking tools using acceleration techniques (like FAST). Finally, we introduce and study a powerful generalization of IO nets: Branching IO nets (BIO nets), in which transitions can create tokens. BIO nets extend both IO nets and BPP nets. We show that, while BIO nets are no longer globally flat, and their sets of reachable markings may be non-semilinear, they are still locally flat. As a consequence, the parameterized coverability and reachability problems remain in PSPACE. This makes BIO nets the first natural net class with non-semilinear reachability relation for which the reachability problem is provably simpler than for general Petri nets.