The Complexity of Boolean State Separation (Technical Report)

10/02/2020

∙

by   Ronny Tredup, et al.

∙

0

∙

share

For a Boolean type of nets τ, a transition system A is synthesizeable into a τ-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 τ-state separation property (τ-SSP) while the latter – τ-event/state separation property (τ-ESSP). A is embeddable into the reachability graph of a τ-net N if and only if A has the τ-SSP. This paper presents a complete characterization of the computational complexity of τ-SSP for all Boolean Petri net types.