Divide-and-Conquer Methods for Synthesis

This chapter describes several general techniques aimed at accelerating Petri net synthesis from labelled transition systems. One technique, called presynthesis, eliminates non-synthesisable transition systems before actual synthesis is started. Other techniques, called divide-and-conquer, aim at exploiting a transition system’s structure in order to speed up synthesis. In the divide-and-conquer approach, the synthesis problem is broken up into several subproblems which are smaller and easier to solve, and whose solution can be combined to an overall solution. One method attempts to detect hidden concurrency in a given transition system, and to determine independent parts which consequently can be factored out. Another method attempts to detect loose couplings between transition system parts, and then to separate these parts into smaller subproblems.