In: IEEE Trans. on Computers, Vol. 44, No. 11, pages 1306-1317. 1995.
Abstract: Determining the time separation of events is a fundamental problem in the analysis, synthesis, and optimization of concurrent systems. Applications range from logic optimization of asynchronous digital circuits to evaluation of execution times of programs for real-time systems. We present an efficient algorithm to find exact (tight) bounds on the separation time of events in an arbitrary process graph without conditional behavior. This result is more general than the methods presented in several previously published papers as it handles cyclic graphs and yields the tightest possible bounds on event separations. The algorithm is based on a functional decomposition technique that permits the implicit evaluation of an infinitely unfolded process graph. Examples are presented that demonstrate the utility and efficiency of the solution, The algorithm will form a basis for exploration of timing-constrained synthesis techniques.
Keywords: Petri nets, abstract algebras, asynchronous systems, concurrent systems, specification verification, system specification, time separation of events, timing verification.