Marked Graph Synthesis

If marked graphs are targeted by synthesis from labelled transition systems, it is possible to devise a very fast algorithm. To this end, the necessary conditions for synthesisability considered earlier can be strengthened to a full characterisation, that is, a set of necessary and sufficient conditions. The present chapter presents a standalone characterisation of the class of (connected, bounded and live) marked graph reachability graphs. A specialised, efficient, synthesis algorithm can be derived from this characterisation and, at the same time, serves as a proof of the latter.