Synthesis of Decision-Free Concurrent Systems for Prescribed Resources and Performance.

This paper presents a method for synthesizing or growing live and safe marked graph models of decision-free concurrent computations. The approach is modular in the sense that subsystems represented by arcs (and nodes) are added one by one without the need of redesigning the entire system. The following properties of marked graph models can be prescribed in the synthesis: liveness (absence of deadlocks), safeness (absence of overflows), the number of reachability classes, the maximum resource (temporary storage) requirement, computation rate (performance), as well as the numbers of arcs and states. [ABSTRACT FROM AUTHOR]