| 電子情報通信学会 研究会発表申込システム 講演論文 詳細 |
技報閲覧サービス [ログイン] 技報アーカイブ |
| トップに戻る | 前のページに戻る | [Japanese] / [English] |
| 講演抄録／キーワード | ||
| 講演名 | 2017-03-09 09:30 クロック凍結機構を持つ稠密時間プッシュダウンオートマトンの記号実行 ○平岡 祥・結縁祥治（名大）  SS2016-60 |
|
| 抄録 | （和） | 本研究では，クロック凍結機構を持つ稠密時間プッシュダウンオートマトン（Dense-Timed Pushdown Automata with Clock Freezing，以下DTPDA-F）の状態到達可能性を保存するゾーン構成手法を示す． Abudullahらによって提案された稠密時間プッシュダウンオートマトン（以下DTPDA）は，時間に依存したプログラムの振る舞いモデルとして提案され，状態到達可能性が決定可能であることが知られている． さらに，Liらによってクロック凍結機構が導入され，一定の条件のもとで状態到達可能性が決定可能であることが示されている． ここで用いられている離散化の技法であるリージョン抽象は構成時に状態数が指数的に増加することが知られており，実用的な検証モデルとしてゾーン構成による効率的な離散化が有効である． クロック凍結機構を導入したDATPA-Fに対して，Ausmeesによるゾーン構成に基づいて効率的に状態到達可能性を検証するゾーンプッシュダウンオートマトン（以下ゾーンPDA）の構成手法を示し，ゾーンPDAがDTPDA-Fの計算を記号的にシミュレート可能であることについての証明を示す． |
| （英） | We present a symbolic simulation based on a zone construction for the dense timed pushdown automata with clock freezing(DTPDA-F) as a discretization method to verify the state reachability property. The dense timed pushdown automata (DTPDA) has been proposed as a behavioral model for time dependent programs by Abdullah et al. Li et al. adds the clock freezing mechanism to DTPDA and showed that the model DTPDA-F preserves the state reachability being decidable under a certain condition. In the literature, to prove the reachability, the region construction method has been used to discretize the behavior of DTPDA-F. Since the region abstraction is known to cause the state explosion in the symbolic simulation, the zone construction needs to be used in practice as seen in the timed automata. We propose a zone construction method for discretization of DTPDA-F behavior extending the construction of Ausmees's intending the verification to be more efficient and prove soundness. |
|
| キーワード | （和） | 時間オートマトン / プッシュダウンオートマトン / ゾーン構成 / クロック凍結 / / / / |
| （英） | Timed Automata / Pushdown automata / Zone consutruction / Clock freezing / / / / | |
| 文献情報 | 信学技報, vol. 116, no. 512, SS2016-60, pp. 1-6, 2017年3月. | |
| 資料番号 | SS2016-60 | |
| 発行日 | 2017-03-02 (SS) | |
| ISSN | Print edition: ISSN 0913-5685 Online edition: ISSN 2432-6380 | |
| 著作権に ついて |
技術研究報告に掲載された論文の著作権は電子情報通信学会に帰属します．(許諾番号：10GA0019/12GB0052/13GB0056/17GB0034/18GB0034) | |
| PDFダウンロード | SS2016-60 |
|
| 研究会情報 | |
| 研究会 | SS |
| 開催期間 | 2017-03-09 - 2017-03-10 |
| 開催地（和） | てんぶす那覇 |
| 開催地（英） | |
| テーマ（和） | 一般 |
| テーマ（英） | |
| 講演論文情報の詳細 | |
| 申込み研究会 | SS |
| 会議コード | 2017-03-SS |
| 本文の言語 | 日本語 |
| タイトル（和） | クロック凍結機構を持つ稠密時間プッシュダウンオートマトンの記号実行 |
| サブタイトル（和） | |
| タイトル（英） | A Symbolic Simulation of Dense-Timed Pushdown Automata with Clock Freezing |
| サブタイトル（英） | |
| キーワード(1)（和/英） | 時間オートマトン / Timed Automata |
| キーワード(2)（和/英） | プッシュダウンオートマトン / Pushdown automata |
| キーワード(3)（和/英） | ゾーン構成 / Zone consutruction |
| キーワード(4)（和/英） | クロック凍結 / Clock freezing |
| キーワード(5)（和/英） | / |
| キーワード(6)（和/英） | / |
| キーワード(7)（和/英） | / |
| キーワード(8)（和/英） | / |
| 第1著者 氏名（和/英/ヨミ） | 平岡 祥 / Sho Hiraoka / ヒラオカ ショウ |
| 第1著者 所属（和/英） | 名古屋大学 (略称： 名大) Nagoya University (略称： Nagoya Univ.) |
| 第2著者 氏名（和/英/ヨミ） | 結縁 祥治 / Shoji Yuen / ユエン ショウジ |
| 第2著者 所属（和/英） | 名古屋大学 (略称： 名大) Nagoya University (略称： Nagoya Univ.) |
| 第3著者 氏名（和/英/ヨミ） | / / |
| 第3著者 所属（和/英） | (略称： ) (略称： ) |
| 第4著者 氏名（和/英/ヨミ） | / / |
| 第4著者 所属（和/英） | (略称： ) (略称： ) |
| 第5著者 氏名（和/英/ヨミ） | / / |
| 第5著者 所属（和/英） | (略称： ) (略称： ) |
| 第6著者 氏名（和/英/ヨミ） | / / |
| 第6著者 所属（和/英） | (略称： ) (略称： ) |
| 第7著者 氏名（和/英/ヨミ） | / / |
| 第7著者 所属（和/英） | (略称： ) (略称： ) |
| 第8著者 氏名（和/英/ヨミ） | / / |
| 第8著者 所属（和/英） | (略称： ) (略称： ) |
| 第9著者 氏名（和/英/ヨミ） | / / |
| 第9著者 所属（和/英） | (略称： ) (略称： ) |
| 第10著者 氏名（和/英/ヨミ） | / / |
| 第10著者 所属（和/英） | (略称： ) (略称： ) |
| 第11著者 氏名（和/英/ヨミ） | / / |
| 第11著者 所属（和/英） | (略称： ) (略称： ) |
| 第12著者 氏名（和/英/ヨミ） | / / |
| 第12著者 所属（和/英） | (略称： ) (略称： ) |
| 第13著者 氏名（和/英/ヨミ） | / / |
| 第13著者 所属（和/英） | (略称： ) (略称： ) |
| 第14著者 氏名（和/英/ヨミ） | / / |
| 第14著者 所属（和/英） | (略称： ) (略称： ) |
| 第15著者 氏名（和/英/ヨミ） | / / |
| 第15著者 所属（和/英） | (略称： ) (略称： ) |
| 第16著者 氏名（和/英/ヨミ） | / / |
| 第16著者 所属（和/英） | (略称： ) (略称： ) |
| 第17著者 氏名（和/英/ヨミ） | / / |
| 第17著者 所属（和/英） | (略称： ) (略称： ) |
| 第18著者 氏名（和/英/ヨミ） | / / |
| 第18著者 所属（和/英） | (略称： ) (略称： ) |
| 講演者 | 第1著者 |
| 発表日時 | 2017-03-09 09:30:00 |
| 発表時間 | 25分 |
| 申込先研究会 | SS |
| 資料番号 | SS2016-60 |
| 巻番号（vol） | vol.116 |
| 号番号（no） | no.512 |
| ページ範囲 | pp.1-6 |
| ページ数 | 6 |
| 発行日 | 2017-03-02 (SS) |
[研究会発表申込システムのトップページに戻る]