2020/10/02 by Tredup, Ronny, Erofeev, Evgeny
#Computational Complexity (cs.CC) #FOS: Computer and information sciences #Logic in Computer Science (cs.LO)
paper · doi:10.48550/arxiv.2010.00825
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.