| Presentation | 2016-11-24 Development and evaluation of on-the-fly model checking for a Petri net verification tool (HiPS) Yojiro Harie, Katsumi Wasaki, |
|---|---|
| PDF Download Page |  PDF download Page Link |
| Abstract(in Japanese) | (See Japanese page) |
| Abstract(in English) | This paper proposes an On-the-fly Fluent Linear Temporal Logic (FLTL) model checker using state space generation based on the Petri net models. The hierarchical Petri net simulator (HiPS) tool is a design and verification environment for Place/Transition nets that can perform model checking for a state space. However, exhaustive model checking, which can be computationally excessive, is required to generate the complete state space. on-the-fly model checking reduces memory space and execution time by parallelizing state space generation and sequence searching. We introduce a on-the-fly model checker for HiPS tool and then verify the liveness properties of model for ABP model. |
| Keyword(in Japanese) | (See Japanese page) |
| Keyword(in English) | Petri net / Model checking / on-the-fly / Linear temporal logic / Event based checking |
| Paper # | CAS2016-63,MSS2016-43 |
| Date of Issue | 2016-11-17 (CAS, MSS) |
| Conference Information | |
| Committee | MSS / CAS / IPSJ-AL |
|---|---|
| Conference Date | 2016/11/24(2days) |
| Place (in Japanese) | (See Japanese page) |
| Place (in English) | Kobe Institute of Computing |
| Topics (in Japanese) | (See Japanese page) |
| Topics (in English) | |
| Chair | Satoshi Yamane(Kanazawa Univ.) / Toshihiko Takahashi(Niigata Univ.) |
| Vice Chair | Morikazu Nakamura(Univ. of Ryukyus) / Mitsuru Hiraki(Renesas) |
| Secretary | Morikazu Nakamura(Yamaguchi Univ.) / Mitsuru Hiraki(Toshiba) / (Tohoku Univ.) |
| Assistant | Hideki Kinjo(Okinawa Univ.) / Toshihiro Tachibana(Shonan Inst. of Tech.) / Yohei Nakamura(Hitachi) |
| Paper Information | |
| Registration To | Technical Committee on Mathematical Systems Science and its applications / Technical Committee on Circuits and Systems / Special Interest Group on Algorithms |
|---|---|
| Language | JPN |
| Title (in Japanese) | (See Japanese page) |
| Sub Title (in Japanese) | (See Japanese page) |
| Title (in English) | Development and evaluation of on-the-fly model checking for a Petri net verification tool (HiPS) |
| Sub Title (in English) | |
| Keyword(1) | Petri net |
| Keyword(2) | Model checking |
| Keyword(3) | on-the-fly |
| Keyword(4) | Linear temporal logic |
| Keyword(5) | Event based checking |
| 1st Author's Name | Yojiro Harie |
| 1st Author's Affiliation | Shinshu University(Shinshu Univ.) |
| 2nd Author's Name | Katsumi Wasaki |
| 2nd Author's Affiliation | Shinshu University(Shinshu Univ.) |
| Date | 2016-11-24 |
| Paper # | CAS2016-63,MSS2016-43 |
| Volume (vol) | vol.116 |
| Number (no) | CAS-315,MSS-316 |
| Page | pp.pp.31-35(CAS), pp.31-35(MSS), |
| #Pages | 5 |
| Date of Issue | 2016-11-17 (CAS, MSS) |