2026-05-12T07:06:57Z https://ipsj.ixsq.nii.ac.jp/oai

oai:ipsj.ixsq.nii.ac.jp:00185720 2025-01-20T02:52:10Z 934:935:9346:9347

複数の局所クロックを持つ時間プッシュダウン・オートマトン Dense-timed Pushdown Automata with Multiple Local Clocks 上里, 友弥 Yuya, Uezato [通常論文] 時間オートマトン，プッシュダウンオートマトン，空性判定問題 本論文では，Abdullaらによって導入されたDense-timed pushdown automata（TPDA）を拡張し，複数の局所クロックを持つTPDAを考え，この拡張が言語クラスを拡大しないことを示す．TPDAは，時間オートマトンとプッシュダウン・オートマトンの両方の性質を持つ計算モデルであり，従来のプッシュダウン・オートマトンにおけるスタックとは異なり，時間付きスタック（クロック付きスタック）を考える．時間付きスタックでは，各要素が1つのスタック記号と1つのクロック（非負実数値をとる変数）の組からなる．今回提案する複数の局所クロックを持つTPDAは，スタックの各要素が1つのスタック記号と複数のクロックからなる拡張といえる．最近になり，TPDAの言語表現能力は，時間オートマトンに時間なしスタック（スタックの各要素が1つのスタック記号からなる通常の意味でのスタック）を付け加えたものと合致するということが，Clementeらによって示された．このことは，言語を保存したままに，TPDAのスタックからクロックをすべて取り去ることができることを意味する．本論文では，Clementeらによる証明手法を基に，提案する拡張についても，言語を保存したままにスタックからクロックをすべて除去できることを証明する． 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. 情報処理学会 2018-02-08 jpn journal article https://ipsj.ixsq.nii.ac.jp/records/185720 1882-7802 AA11464814 情報処理学会論文誌プログラミング（PRO） 11 1 10 28 https://ipsj.ixsq.nii.ac.jp/record/185720/files/IPSJ-TPRO1101006.pdf application/pdf 517.5 kB 2020-02-08