首页    期刊浏览 2024年11月29日 星期五
登录注册

文章基本信息

  • 标题:同期型再帰的時間オートマトンの到達可能性解析
  • 本地全文:下载
  • 作者:上里 友弥 ; 南出 靖彦
  • 期刊名称:コンピュータ ソフトウェア
  • 印刷版ISSN:0289-6540
  • 出版年度:2018
  • 卷号:35
  • 期号:1
  • 页码:1_140-1_168
  • DOI:10.11309/jssst.35.1_140
  • 语种:Japanese
  • 出版社:Japan Society for Software Science and Technology
  • 摘要:

    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.

国家哲学社会科学文献中心版权所有