電子情報通信学会 研究会発表申込システム
講演論文 詳細
技報閲覧サービス
技報オンライン
‥‥ (ESS/通ソ/エレソ/ISS)
技報アーカイブ
‥‥ (エレソ)
 トップに戻る 前のページに戻る   [Japanese] / [English] 

講演抄録/キーワード
講演名 2016-10-27 15:05
クロック凍結機構を持つ稠密時間プッシュダウンオートマトンのゾーン構成による検証
平岡 祥結縁祥治名大
技報オンラインサービス実施中
抄録 (和) 本研究では、クロック凍結機構を持つ稠密時間プッシュダウンオートマトンの状態到達可能性を保存するゾーン構成手法を提案する。
Abudullah らによって提案された稠密時間プッシュダウンオートマトン(DTPDA) は、時間に依存したプログラムのモデルとして提案され、状態到達可能性が決定可能であることが知られている。
さらに、Li らによってクロック凍結機構が導入され、ある条件のもとでは状態到達可能性が決定可能であることが示されている。
時間経過は稠密時間であるため、これらの議論においては離散化のためのリージョン構成が提案されている。
Ausmees によるDTPDA のゾーン構成を拡張し、クロック凍結を導入して、状態到達可能性を保存するゾーンプッシュダウンオートマトンの構成を示す。 
(英) We present a zone construction for the dense timed pushdown automata with freezing ages as a discretization method to verify the state reachablity property.
The dense timed pushdown automata (DTPDA) by Abdullah et el. has been proposed as a behavioral model for time dependent programs with the decidability of the state reachability.
Li et al. shows the clock freezing mechanism added to DTPDA (DTDPA-F) still preserves the state reachability under some condition.
To prove the reachability, a region construction method was used to discretize DTPDA and DTPDA-F.
We propose a zone construction method for discretization of DTPDA-F extending
that by Ausmees to make the verificaiton more efficient.
キーワード (和) 時間オートマトン / プッシュダウンオートマトン / ゾーン構成 / クロック凍結 / / / /  
(英) Timed Automata / Pushdown automata / Zone consutruction / Clock freezing / / / /  
文献情報 信学技報, vol. 116, no. 277, SS2016-25, pp. 43-48, 2016年10月.
資料番号 SS2016-25 
発行日 2016-10-20 (SS, DC) 
ISSN Print edition: ISSN 0913-5685  Online edition: ISSN 2432-6380

研究会情報
研究会 DC SS  
開催期間 2016-10-27 - 2016-10-28 
開催地(和) 彦根勤労福祉会館(彦根市) 
開催地(英) Hikone Kinro-Fukushi Kaikan Bldg. 
テーマ(和) ソフトウェアシステム, ネットワーク環境でのディペンダビリティ 
テーマ(英) Software System and Dependability on Network, etc 
講演論文情報の詳細
申込み研究会 SS 
会議コード 2016-10-DC-SS 
本文の言語 日本語 
タイトル(和) クロック凍結機構を持つ稠密時間プッシュダウンオートマトンのゾーン構成による検証 
サブタイトル(和)  
タイトル(英) Towards a Zone-based Verification for DTPDA 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著者 所属(和/英) (略称: )
(略称: )
第19著者 氏名(和/英/ヨミ) / /
第19著者 所属(和/英) (略称: )
(略称: )
第20著者 氏名(和/英/ヨミ) / /
第20著者 所属(和/英) (略称: )
(略称: )
講演者
発表日時 2016-10-27 15:05:00 
発表時間 25 
申込先研究会 SS 
資料番号 IEICE-SS2016-25,IEICE-DC2016-27 
巻番号(vol) IEICE-116 
号番号(no) no.277(SS), no.278(DC) 
ページ範囲 pp.43-48 
ページ数 IEICE-6 
発行日 IEICE-SS-2016-10-20,IEICE-DC-2016-10-20 


[研究会発表申込システムのトップページに戻る]

[電子情報通信学会ホームページ]


IEICE / 電子情報通信学会