next up previous
Next: Fair parametric extended automata Up: Analyzing new types of Previous: Systems modeled by timed

Systems with real variables

Previous work has shown that the combined linear arithmetic of real and integer variables can be dealt with by using finite automata on infinite words. Unfortunately, this involves some difficult and delicate to implement algorithms. In [BJW01], it is shown, using topological arguments, that only a restricted class of automata on infinite words are necessary for handling real and integer linear arithmetic. This allows the use of substantially simpler algorithms and opens the path to the implementation of a usable system for handling this combined theory. The results of this paper have indeed been implemented and made available in the tool LASH [LAS]. The application of these results to the symbolic state-space exploration of timed systems is the subject of ongoing work.