| Presentation | 2020-10-19 LTL Model Checking for Register Pushdown Systems Ryoma Senda, Yoshiaki Takata, Hiroyuki Seki, |
|---|---|
| PDF Download Page |  PDF download Page Link |
| Abstract(in Japanese) | (See Japanese page) |
| Abstract(in English) | 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. |
| Keyword(in Japanese) | (See Japanese page) |
| Keyword(in English) | register pushdown systemLTL model checkingregularity preservationregister automaton |
| Paper # | SS2020-6,DC2020-23 |
| Date of Issue | 2020-10-12 (SS, DC) |
| Conference Information | |
| Committee | DC / SS |
|---|---|
| Conference Date | 2020/10/19(1days) |
| Place (in Japanese) | (See Japanese page) |
| Place (in English) | Online |
| Topics (in Japanese) | (See Japanese page) |
| Topics (in English) | |
| Chair | Hiroshi Takahashi(Ehime Univ.) / Takashi Kobayashi(Tokyo Inst. of Tech.) |
| Vice Chair | Tatsuhiro Tsuchiya(Osaka Univ.) / Kozo Okano(Shinshu Univ.) |
| Secretary | Tatsuhiro Tsuchiya(Nihon Univ.) / Kozo Okano(Chiba Univ.) |
| Assistant | / Shinpei Ogata(Shinshu Univ.) |
| Paper Information | |
| Registration To | Technical Committee on Dependable Computing / Technical Committee on Software Science |
|---|---|
| Language | ENG |
| Title (in Japanese) | (See Japanese page) |
| Sub Title (in Japanese) | (See Japanese page) |
| Title (in English) | LTL Model Checking for Register Pushdown Systems |
| Sub Title (in English) | |
| Keyword(1) | register pushdown systemLTL model checkingregularity preservationregister automaton |
| 1st Author's Name | Ryoma Senda |
| 1st Author's Affiliation | Nagoya University(Nagoya Univ.) |
| 2nd Author's Name | Yoshiaki Takata |
| 2nd Author's Affiliation | Kochi University of Technology(KUT) |
| 3rd Author's Name | Hiroyuki Seki |
| 3rd Author's Affiliation | Nagoya University(Nagoya Univ.) |
| Date | 2020-10-19 |
| Paper # | SS2020-6,DC2020-23 |
| Volume (vol) | vol.120 |
| Number (no) | SS-193,DC-194 |
| Page | pp.pp.7-12(SS), pp.7-12(DC), |
| #Pages | 6 |
| Date of Issue | 2020-10-12 (SS, DC) |