| 講演名 | 2020-10-19 LTL Model Checking for Register Pushdown Systems 仙田 涼摩(名大), 高田 喜朗(高知工科大), 関 浩之(名大), |
|---|---|
| PDFダウンロードページ |  PDFダウンロードページへ |
| 抄録(和) | A pushdown system (PDS) is known as an abstract model of recursive programs. For PDS, model checking methods have been studied andapplied to various software verification such as interprocedural data flow analysis and malware detection. However, PDS cannot manipulate data values. A register PDS (RPDS) is an extension of PDS by adding registers to deal with data values in a restricted way. This paper proposes algorithms for LTL model checking problems for RPDS with simple and regular valuations, which are labelings of atomic propositions to configurations with reasonable restriction. First, we introduce RPDS and related models, and then define the LTL model checking problems for RPDS. Second, we give algorithms for solving these problems and also show thatthe problems are EXPTIME-complete. An example taken from XML schema checking is also given. |
| 抄録(英) | A pushdown system (PDS) is known as an abstract model of recursive programs. For PDS, model checking methods have been studied andapplied to various software verification such as interprocedural data flow analysis and malware detection. However, PDS cannot manipulate data values. A register PDS (RPDS) is an extension of PDS by adding registers to deal with data values in a restricted way. This paper proposes algorithms for LTL model checking problems for RPDS with simple and regular valuations, which are labelings of atomic propositions to configurations with reasonable restriction. First, we introduce RPDS and related models, and then define the LTL model checking problems for RPDS. Second, we give algorithms for solving these problems and also show thatthe problems are EXPTIME-complete. An example taken from XML schema checking is also given. |
| キーワード(和) | |
| キーワード(英) | register pushdown systemLTL model checkingregularity preservationregister automaton |
| 資料番号 | SS2020-6,DC2020-23 |
| 発行日 | 2020-10-12 (SS, DC) |
| 研究会情報 | |
| 研究会 | DC / SS |
|---|---|
| 開催期間 | 2020/10/19(から1日開催) |
| 開催地（和） | オンライン開催 |
| 開催地（英） | Online |
| テーマ（和） | ソフトウェアシステムとディペンダブルコンピューティングおよび一般 |
| テーマ（英） | |
| 委員長氏名（和） | 高橋 寛(愛媛大) / 小林 隆志(東工大) |
| 委員長氏名（英） | Hiroshi Takahashi(Ehime Univ.) / Takashi Kobayashi(Tokyo Inst. of Tech.) |
| 副委員長氏名（和） | 土屋 達弘(阪大) / 岡野 浩三(信州大) |
| 副委員長氏名（英） | Tatsuhiro Tsuchiya(Osaka Univ.) / Kozo Okano(Shinshu Univ.) |
| 幹事氏名（和） | 新井 雅之(日大) / 難波 一輝(千葉大) / 島 和之(広島市大) / 林 晋平(東工大) |
| 幹事氏名（英） | Masayuki Arai(Nihon Univ.) / Kazuteru Namba(Chiba Univ.) / Kazuyuki Shima(Hiroshima City Univ.) / Shinpei Hayashi(Tokyo Inst. of Tech.) |
| 幹事補佐氏名（和） | / 小形 真平(信州大) |
| 幹事補佐氏名（英） | / Shinpei Ogata(Shinshu Univ.) |
| 講演論文情報詳細 | |
| 申込み研究会 | Technical Committee on Dependable Computing / Technical Committee on Software Science |
|---|---|
| 本文の言語 | ENG |
| タイトル（和） | |
| サブタイトル（和） | |
| タイトル（英） | LTL Model Checking for Register Pushdown Systems |
| サブタイトル（和） | |
| キーワード(1)（和/英） | / register pushdown systemLTL model checkingregularity preservationregister automaton |
| 第 1 著者 氏名（和/英） | 仙田 涼摩 / Ryoma Senda |
| 第 1 著者 所属（和/英） | 名古屋大学(略称：名大) Nagoya University(略称：Nagoya Univ.) |
| 第 2 著者 氏名（和/英） | 高田 喜朗 / Yoshiaki Takata |
| 第 2 著者 所属（和/英） | 高知工科大学(略称：高知工科大) Kochi University of Technology(略称：KUT) |
| 第 3 著者 氏名（和/英） | 関 浩之 / Hiroyuki Seki |
| 第 3 著者 所属（和/英） | 名古屋大学(略称：名大) Nagoya University(略称：Nagoya Univ.) |
| 発表年月日 | 2020-10-19 |
| 資料番号 | SS2020-6,DC2020-23 |
| 巻番号（vol） | vol.120 |
| 号番号（no） | SS-193,DC-194 |
| ページ範囲 | pp.7-12(SS), pp.7-12(DC), |
| ページ数 | 6 |
| 発行日 | 2020-10-12 (SS, DC) |