複数の局所クロックを持つ時間プッシュダウン・オートマトン

• Item type: Trans(1)
• 公開日: 2018-02-08
• タイトル: 複数の局所クロックを持つ時間プッシュダウン・オートマトン
• タイトル / 言語: en
• タイトル: Dense-timed Pushdown Automata with Multiple Local Clocks
• 言語: jpn
• キーワード / 主題Scheme: Other
• キーワード / 主題: [通常論文] 時間オートマトン，プッシュダウンオートマトン，空性判定問題
• 資源タイプ / 資源タイプ識別子: http://purl.org/coar/resource_type/c_6501
• 資源タイプ: journal article
• 著者所属: 筑波大学システム情報工学研究科コンピュータサイエンス専攻
• 著者所属(英): en
• 著者所属(英): Department of Computer Science, Graduate School of SIE, University of Tsukuba
• 著者名: 上里, 友弥
• 著者名(英): Yuya, Uezato
• 論文抄録 / 内容記述タイプ: Other
• 論文抄録 / 内容記述: 本論文では，Abdullaらによって導入されたDense-timed pushdown automata（TPDA）を拡張し，複数の局所クロックを持つTPDAを考え，この拡張が言語クラスを拡大しないことを示す．TPDAは，時間オートマトンとプッシュダウン・オートマトンの両方の性質を持つ計算モデルであり，従来のプッシュダウン・オートマトンにおけるスタックとは異なり，時間付きスタック（クロック付きスタック）を考える．時間付きスタックでは，各要素が1つのスタック記号と1つのクロック（非負実数値をとる変数）の組からなる．今回提案する複数の局所クロックを持つTPDAは，スタックの各要素が1つのスタック記号と複数のクロックからなる拡張といえる．最近になり，TPDAの言語表現能力は，時間オートマトンに時間なしスタック（スタックの各要素が1つのスタック記号からなる通常の意味でのスタック）を付け加えたものと合致するということが，Clementeらによって示された．このことは，言語を保存したままに，TPDAのスタックからクロックをすべて取り去ることができることを意味する．本論文では，Clementeらによる証明手法を基に，提案する拡張についても，言語を保存したままにスタックからクロックをすべて除去できることを証明する．
• 論文抄録(英) / 内容記述タイプ: Other
• 論文抄録(英) / 内容記述: We present a new extension of dense-timed pushdown automata (TPDA) called TPDA with multiple local clocks and show the language classes of TPDA and TPDA with multiple local clocks are the same. Abdulla et al. introduced TPDA as a timed extension of pushdown automata. A TPDA can be seen as a timed automaton with a timed stack in which each element is a pair of one stack symbol and one real-valued clock variable. Our TPDA with multiple local clocks can be seen as a timed automaton with a timed stack in which each element consists of one stack symbol and multiple clock variables. Recently, Clemente and Lasota showed that the language class of TPDA equals to the language class of timed automata with an untimed stack. In other words, they showed that we can remove all the clock variables in the timed stack of a given TPDA while preserving its language. In the present paper, as the untiming result of TPDA, we show that all the clock variables in the timed stack of a given TPDA with multiple local clocks can be removed while preserving its language.
• 書誌レコードID / 収録物識別子タイプ: NCID
• 書誌レコードID / 収録物識別子: AA11464814
• 書誌情報: 情報処理学会論文誌プログラミング（PRO）; 巻 11, 号 1, p. 10-28, 発行日 2018-02-08
• ISSN / 収録物識別子タイプ: ISSN
• ISSN / 収録物識別子: 1882-7802
• 出版者 / 言語: ja
• 出版者: 情報処理学会