The Complexity of Boolean State Separation (Technical Report)

TL;DR

This paper characterizes the computational complexity of the state separation problem in Boolean Petri nets, providing a comprehensive understanding of when such nets can be synthesized from transition systems.

Contribution

It offers a complete complexity classification of the $ au$-state separation property for all Boolean Petri net types, advancing theoretical understanding.

Findings

Provides complexity classifications for $ au$-SSP across all Boolean Petri net types.

Establishes conditions under which a transition system can be embedded into a $ au$-net.

Clarifies the relationship between $ au$-SSP and $ au$-ESSP in net synthesis.

Abstract

For a Boolean type of nets $\tau$, a transition system $A$ is synthesizeable into a $\tau$-net $N$ if and only if distinct states of $A$ correspond to distinct markings of $N$, and $N$ prevents a transition firing if there is no related transition in $A$. The former property is called $\tau$-state separation property ($\tau$-SSP) while the latter -- $\tau$-event/state separation property ($\tau$-ESSP). $A$ is embeddable into the reachability graph of a $\tau$-net $N$ if and only if $A$ has the $\tau$-SSP. This paper presents a complete characterization of the computational complexity of \textsc{$\tau$-SSP} for all Boolean Petri net types.