Analyzing Timed Systems Using Tree Automata

Timed systems, such as timed automata, are usually analyzed using theiroperational semantics on timed words. The classical region abstraction fortimed automata reduces them to (untimed) finite state automata with the sametime-abstract properties, such as state reachability. We propose a newtechnique to analyze such timed systems using finite tree automata instead offinite word automata. The main idea is to consider timed behaviors as graphswith matching edges capturing timing constraints. When a family of graphs hasbounded tree-width, they can be interpreted in trees and MSO-definableproperties of such graphs can be checked using tree automata. The technique isquite general and applies to many timed systems. In this paper, as an example,we develop the technique on timed pushdown systems, which have recentlyreceived considerable attention. Further, we also demonstrate how we can use iton timed automata and timed multi-stack pushdown systems (with boundednessrestrictions)