The Complexity of Boolean State Separation (Technical Report)
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.
READ FULL TEXT