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