In: PNPM89. Proceedings of the Third International Workshop On Petri Nets and Performance Models, 1989, Kyoto, Japan, pages 266-276. Los Alamitos, CA, USA: IEEE Computer Society Press, 1990.
Abstract: Synthesis relieves the complexity problems which may be encountered in verification of concurrent systems by avoiding verification. Petri nets are used for modeling concurrent sytems. The ``Temporal Matrix'' is used to record relationship among processes and to detect rule violations. A set of synthesis rules was developed for incrementally generating new processes without incurring logical incorrectness. The paper develops an algorithm to detect rule violations and to update the Temporal Matrix. The complexity of the algorithm is polynomial and O(N³), where N is the total number of pseudo-processes.
Keywords: synthesis technique; temporal matrix.