Algebraic Techniques for Timed Systems

Performance evaluation is a central issue in the design of complex real-time systems. In this work, we propose an extension of socalled "Max-Plus" algebraic techniques to handle more realistic types of real-time systems. In particular, our framework encompasses graph or partial order automata, and more generally abstract models of real-time computations (including synchronous programs running over distributed architectures). To achieve this, we introduce a new dioid of partially commutative power series (transductions), whose elements encode timed behaviors. This formalism extends the traditional representation of timed event graphs by (rational) commutative transfer series with coefficients in the Max-Plus semiring. We sketch how this framework can be used to symbolically solve several problems of interest, related to real-time systems. Then we illustrate the use of this framework to encode a nontrivial mixed formalism of dataliow diagrams and automata.