The time separation of events (TSE) problem is that of finding the
maximum and minimum separation between the times of occurrence of two events
in a concurrent system.
It has applications in the performance analysis,
optimization and verification of concurrent digital systems.
This paper introduces an efficient polynomial-time algorithm to give
exact bounds on TSE's
for choice-free concurrent systems, whose operational semantics obey
the max-causality rule.
A choice-free concurrent system is modeled as a strongly-connected
marked graph, where delays on operations
are modeled as bounded intervals with unspecified distributions.
While previous approaches handle acyclic systems only, or else require
graph unfolding until a steady-state behavior is reached, the proposed
approach directly identifies and evaluates the asymptotic
steady-state behavior of a cyclic system via a graph-theoretical approach.
As a result, the method has significantly lower computational complexity
than previously-proposed solutions.
A prototype CAD tool has been developed
to demonstrate the feasibility and efficacy of our method.
A set of experiments have been performed on the tool as well as two
existing tools, with noticeable improvement on runtime and accuracy for
several examples.