| Presentation | 2020-03-03 Model checking RNNs with modal μ-calculus Tatsuhiro Aoshima, Toshinori Usui, |
|---|---|
| PDF Download Page |  PDF download Page Link |
| Abstract(in Japanese) | (See Japanese page) |
| Abstract(in English) | Machine learning models have been applied to many cyber-physical systems such as self-driving cars, robotics, and factory automation. However, it would be difficult to adapt them to more mission-critical systems, such as energy plants, because there is no safety guarantee. This paper presents the security of systems controlled using machine learning models, especially, Recurrent Neural Networks (RNNs). We propose a novel method for checking whether a given RNN satisfies a given specification, as abstractly interpreting the model with the con-strained zonotopes. The specification is written in the modal μ-calculus containing many classical temporal logics such as Linear Temporal Logic and Computation Tree Logic. |
| Keyword(in Japanese) | (See Japanese page) |
| Keyword(in English) | Model checking / Recurrent Neural Networks / Modal μ-calculus / Constrained zonotopes |
| Paper # | ICSS2019-88 |
| Date of Issue | 2020-02-24 (ICSS) |
| Conference Information | |
| Committee | ICSS / IPSJ-SPT |
|---|---|
| Conference Date | 2020/3/2(2days) |
| Place (in Japanese) | (See Japanese page) |
| Place (in English) | Okinawa-Ken-Seinen-Kaikan |
| Topics (in Japanese) | (See Japanese page) |
| Topics (in English) | Security, Trust, etc. |
| Chair | Hiroki Takakura(NII) |
| Vice Chair | Katsunari Yoshioka(Yokohama National Univ.) / Kazunori Kamiya(NTT) |
| Secretary | Katsunari Yoshioka(NICT) / Kazunori Kamiya(KDDI labs.) |
| Assistant | Keisuke Kito(Mitsubishi Electric) / Toshihiro Yamauchi(Okayama Univ.) |
| Paper Information | |
| Registration To | Technical Committee on Information and Communication System Security / Special Interest Group on Security Psychology and Trust |
|---|---|
| Language | JPN |
| Title (in Japanese) | (See Japanese page) |
| Sub Title (in Japanese) | (See Japanese page) |
| Title (in English) | Model checking RNNs with modal μ-calculus |
| Sub Title (in English) | |
| Keyword(1) | Model checking |
| Keyword(2) | Recurrent Neural Networks |
| Keyword(3) | Modal μ-calculus |
| Keyword(4) | Constrained zonotopes |
| 1st Author's Name | Tatsuhiro Aoshima |
| 1st Author's Affiliation | NTT Secure Platform Laboratories(NTT) |
| 2nd Author's Name | Toshinori Usui |
| 2nd Author's Affiliation | NTT Secure Platform Laboratories(NTT) |
| Date | 2020-03-03 |
| Paper # | ICSS2019-88 |
| Volume (vol) | vol.119 |
| Number (no) | ICSS-437 |
| Page | pp.pp.119-124(ICSS), |
| #Pages | 6 |
| Date of Issue | 2020-02-24 (ICSS) |