| Presentation | 2021-03-03 A Subclass of LTL with the Freeze Quantifier Translatable into Register Automata Akira Onishi, Ryoma Senda, Yoshiaki Takata, Hiroyuki Seki, |
|---|---|
| PDF Download Page |  PDF download Page Link |
| Abstract(in Japanese) | (See Japanese page) |
| Abstract(in English) | Register automaton (abbreviated as RA) is an extension of finite automaton by addingregisters storing data values. RA has good properties such that the membership and emptiness problems are decidable. LTL with the freeze quantifier (abbreviated as LTL$^downarrow$) is a counterpart of RA. However, the expressive power of LTL$^downarrow$ is too high to be applied to automatic verification. In this paper, we propose a subclass of LTL$^downarrow$ that can be translated into RA and provide a translation from this subclass to RA. In a general LTL$^downarrow$ formula, a conjunct $psi_1 wedge psi_2$ cannot be simulated by RA. The proposed subclass is defined by prohibiting at least one of $psi_1$ and $psi_2$ containing freeze quantifier or temporal operator other than $X$. |
| Keyword(in Japanese) | (See Japanese page) |
| Keyword(in English) | LTL with the freeze quantifier / register automaton / equivalence translation / model checking |
| Paper # | SS2020-29 |
| Date of Issue | 2021-02-24 (SS) |
| Conference Information | |
| Committee | SS |
|---|---|
| Conference Date | 2021/3/3(2days) |
| Place (in Japanese) | (See Japanese page) |
| Place (in English) | Online |
| Topics (in Japanese) | (See Japanese page) |
| Topics (in English) | |
| Chair | Takashi Kobayashi(Tokyo Inst. of Tech.) |
| Vice Chair | Kozo Okano(Shinshu Univ.) |
| Secretary | Kozo Okano(Hiroshima City Univ.) |
| Assistant | Shinpei Ogata(Shinshu Univ.) |
| Paper Information | |
| Registration To | Technical Committee on Software Science |
|---|---|
| Language | JPN |
| Title (in Japanese) | (See Japanese page) |
| Sub Title (in Japanese) | (See Japanese page) |
| Title (in English) | A Subclass of LTL with the Freeze Quantifier Translatable into Register Automata |
| Sub Title (in English) | |
| Keyword(1) | LTL with the freeze quantifier |
| Keyword(2) | register automaton |
| Keyword(3) | equivalence translation |
| Keyword(4) | model checking |
| 1st Author's Name | Akira Onishi |
| 1st Author's Affiliation | Nagoya University(Nagoya Univ.) |
| 2nd Author's Name | Ryoma Senda |
| 2nd Author's Affiliation | Nagoya University(Nagoya Univ.) |
| 3rd Author's Name | Yoshiaki Takata |
| 3rd Author's Affiliation | Kochi University of Technology(KUT) |
| 4th Author's Name | Hiroyuki Seki |
| 4th Author's Affiliation | Nagoya University(Nagoya Univ.) |
| Date | 2021-03-03 |
| Paper # | SS2020-29 |
| Volume (vol) | vol.120 |
| Number (no) | SS-407 |
| Page | pp.pp.7-12(SS), |
| #Pages | 6 |
| Date of Issue | 2021-02-24 (SS) |