Partial-Order Reduction for Performance Analysis of Max-Plus Timed Systems

This paper presents a partial-order reduction method for performance analysis of max-plus timed systems. A max-plus timed system is a network of automata, where the timing behavior of deterministic system tasks (events in an automaton) is captured in (max, +) matrices. These tasks can be characterized in various formalisms like synchronous data flow, Petri nets, or real-time calculus. The timing behavior of the system is captured in a (max, +) state space, calculated from the composition of the automata. This state space may exhibit redundant interleaving with respect to performance aspects like throughput or latency. The goal of this work is to obtain a smaller state space to speed up performance analysis. To achieve this, we first formalize state-space equivalence with respect to throughput and latency analysis. Then, we present a way to compute a reduced composition directly from the specification. This yields a smaller equivalent state space. We perform the reduction on-the-fly, without first computing the full composition. Experiments show the effectiveness of the method on a set of realistic manufacturing system models.