| Presentation | 2021-10-19 A Subclass of Mu-Calculus with the Freeze Quantifier Equivalent to 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. In the previous study, we proposed a subclass of LTL with the freeze quantifier that can be translated into RA. However, the expressive power of the subclass is weaker than that of RA. In this paper, we propose a subclass of mu-calculus with the freeze quantifier, provide equivalent translations between this subclass and RA, and show their correctness. |
| Keyword(in Japanese) | (See Japanese page) |
| Keyword(in English) | mu-calculus with the freeze quantifier / register automaton / equivalence translation / model checking |
| Paper # | SS2021-17,DC2021-22 |
| Date of Issue | 2021-10-12 (SS, DC) |
| Conference Information | |
| Committee | SS / DC |
|---|---|
| Conference Date | 2021/10/19(1days) |
| 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.) / Hiroshi Takahashi(Ehime Univ.) |
| Vice Chair | Kozo Okano(Shinshu Univ.) / Tatsuhiro Tsuchiya(Osaka Univ.) |
| Secretary | Kozo Okano(Hiroshima City Univ.) / Tatsuhiro Tsuchiya(Tokyo Inst. of Tech.) |
| Assistant | Shinpei Ogata(Shinshu Univ.) |
| Paper Information | |
| Registration To | Technical Committee on Software Science / Technical Committee on Dependable Computing |
|---|---|
| Language | JPN |
| Title (in Japanese) | (See Japanese page) |
| Sub Title (in Japanese) | (See Japanese page) |
| Title (in English) | A Subclass of Mu-Calculus with the Freeze Quantifier Equivalent to Register Automata |
| Sub Title (in English) | |
| Keyword(1) | mu-calculus 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-10-19 |
| Paper # | SS2021-17,DC2021-22 |
| Volume (vol) | vol.121 |
| Number (no) | SS-204,DC-205 |
| Page | pp.pp.23-28(SS), pp.23-28(DC), |
| #Pages | 6 |
| Date of Issue | 2021-10-12 (SS, DC) |