Modeling Real-Time Systems using Rate Automata

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 rim at rates other than one. The extension is well suited to the analysis of scheduling problems, find we demonstrate this by the modeling a simple scheduling policy. We give conditions for reduction of the rate automaton to a finite state automaton.