2018/06/10 by Ronny Tredup, Tredup, Ronny, Christian Rosenke +1
Computer Science · #Computational Complexity (cs.CC) #FOS: Computer and information sciences #Formal Methods in Verification #Model-Driven Software Engineering Techniques #Petri Nets in System Modeling
paper · pdf · doi:10.48550/arxiv.1806.03703
openalex publication_date 2018/06/10 · openalex created_date 2022/10/03 · openalex updated_date 2026/08/04
Boolean nets are Petri nets that permit at most one token per place. Research\nhas approached this important subject in many ways which resulted in various\ndifferent classes of boolean nets. But yet, they are only distinguished by the\nallowed interactions between places and transitions, that is, the possible\neffects of firing transitions. There are eight different interactions: no\noperation (nop), input (inp), output (out), set, reset (res), swap, test of\noccupation (used), and test of disposability (free). Considering every\ncombination for a possible net class yields 256 boolean classes in total. The\nsynthesis problem for a particular class is to take an automaton A and compute\na boolean net of that class that has a state graph isomorphic to A. To the best\nof our knowledge, the computational complexity of this problem has been\nanalyzed for just two of the 256 classes, namely elementary nets systems (nop,\ninp, out), where the problem is NP-hard, and flip-flop nets (nop, inp, out,\nswap), which are synthesizable in polynomial time. However, depending on the\ndesired net features, like read-only places, exception handling, or hierarchy,\none has to synthesize nets with other interactions as for instance contextual\nnets (nop, inp, out, used, free) or trace nets (nop, inp, out, set, res, used,\nfree). The contribution of this paper is a thorough investigation of the\nsynthesis complexity for the 128 boolean net classes that allow nop. Our main\nresult is a general proof scheme that identifies 77 NP-hard cases. All\nremaining 51 classes are shown to be synthesizable in polynomial time where 35\nof them turn out to be trivial.\n