同期型再帰的時間オートマトンの到達可能性解析

摘要

We present synchronized recursive timed automata (SRTA) that extend timed automata with a stack in which each frame contains multiple real valued clocks. SRTA are an extension of dense-timed pushdown automata (TPDA) of Abdulla et al. As with TPDA, timed transitions of an SRTA synchronously increase the values of all the clocks within its stack at the same rate. Our contribution is to show the decidability of the configuration reachability problem of SRTA. On the basis of a thorough study of the proof structure of Abdulla et al., we present a simpler and more modular proof that applies several abstractions to the concrete semantics and consists of their forward and backward simulations. Our proof enables to extend their decidability result of the location reachability problem to the configuration reachability problem of SRTA. We use the region designed by Abdulla et al. for TPDA instead of the conventional region in the theory of timed automata to establish a key technical lemma.