Synthesis of marked graph computation models for prescribed resources and performance
Tadao Murata · 2005
This paper presents a method for synthesizing 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.