| Presentation | 2015-01-26 A Consideration on How to Model Check Distributed Snapshot Reachability Property Wenjie ZHANG, Kazuhiro OGATA, Min ZHANG, |
|---|---|
| PDF Download Page |  PDF download Page Link |
| Abstract(in Japanese) | (See Japanese page) |
| Abstract(in English) | The Chandy-Lamport Distributed Snapshot Algorithm (CLDSA) can determine a consistent global state (called a snapshot) of a distributed system during its computation. Let s_1 be the state when the CLDSA starts, s_* be the snapshot, and s_2 be the state when the CLDSA terminates. The CLDSA should enjoy the property that s_* is always reachable from s_1 and s_2 is always reachable from s_*. The property is called the Distributed Snapshot Reachability (DSR) property. It is not straightforward to express the DSR property in existing temporal logics such as LTL and CTL. We consider how to express the DSR property. |
| Keyword(in Japanese) | (See Japanese page) |
| Keyword(in English) | distributed snapshot / distributed system / model checking / reachability property |
| Paper # | MSS2014-77,SS2014-41 |
| Date of Issue |
| Conference Information | |
| Committee | MSS |
|---|---|
| Conference Date | 2015/1/19(1days) |
| Place (in Japanese) | (See Japanese page) |
| Place (in English) | |
| Topics (in Japanese) | (See Japanese page) |
| Topics (in English) | |
| Chair | |
| Vice Chair | |
| Secretary | |
| Assistant | |
| Paper Information | |
| Registration To | Mathematical Systems Science and its applications(MSS) |
|---|---|
| Language | ENG |
| Title (in Japanese) | (See Japanese page) |
| Sub Title (in Japanese) | (See Japanese page) |
| Title (in English) | A Consideration on How to Model Check Distributed Snapshot Reachability Property |
| Sub Title (in English) | |
| Keyword(1) | distributed snapshot |
| Keyword(2) | distributed system |
| Keyword(3) | model checking |
| Keyword(4) | reachability property |
| 1st Author's Name | Wenjie ZHANG |
| 1st Author's Affiliation | Japan Advanced Institute of Science and Technology, JAIST() |
| 2nd Author's Name | Kazuhiro OGATA |
| 2nd Author's Affiliation | Japan Advanced Institute of Science and Technology, JAIST |
| 3rd Author's Name | Min ZHANG |
| 3rd Author's Affiliation | East China Normal University, ECNU |
| Date | 2015-01-26 |
| Paper # | MSS2014-77,SS2014-41 |
| Volume (vol) | vol.114 |
| Number (no) | 415 |
| Page | pp.pp.- |
| #Pages | 6 |
| Date of Issue | |