Recently, real-time system models have been proposed which fall into the general category of timed automata. A timed automaton consists of a discrete event component represented as a finite automaton, coupled with a temporal component represented as a finite collection of clocks marking time between event occurrences. For timed automata it is possible to reduce certain verification problems to those of checking language containment or language emptiness. We extend this model to allow the clocks to run at rates other than one. The extension is well suited to the analysis of scheduling problems, and we demonstrate this by the modeling a simple scheduling policy. We give conditions for reduction of the rate automaton to a finite state automaton.

Back to Discret Event Systems, Manufacturing Systems, and Communiation Networks Table of Contents