A "Symbolic" Representation of Object-Nets (Extended Version)

TL;DR

This paper extends Petri net morphisms to Elementary Object Systems, enabling nested Petri nets, and uses automorphisms to identify symmetries, reducing the state space for complex systems.

Contribution

It introduces a symbolic representation for Object-Nets by extending Petri net morphisms to nested structures and applying automorphisms for symmetry reduction.

Findings

Nested Petri nets increase reachability graph size

Automorphisms identify symmetries in Petri net topology

Symmetry reduction condenses the state space

Abstract

In this contribution we extend the concept of a Petri net morphism to Elementary Object Systems (EOS). EOS are a nets-within-nets formalism, i.e. we allow the tokens of a Petri net to be Petri nets again. This nested structure has the consequence that even systems defined by very small Petri nets have a quite huge reachability graph. In this contribution we use automorphism to describe symmetries of the Petri net topology. Since these symmetries carry over to markings as well this leads to a condensed state space, too.