| Presentation | 2002/11/21 Parametric Model Checking of Concurrent Periodic EFSMs and an Efficient Simplification Method of Parameter Conditions Fumihiko MASUDA, Takanori MORI, Akio NAKATA, Teruo HIGASHINO, |
|---|---|
| PDF Download Page | PDF download Page Link |
| Abstract(in Japanese) | (See Japanese page) |
| Abstract(in English) | In this paper, we develop a parametric model checking method for concurrent periodic EFSMs and a property described in a real-time extension of CTL(RPCTL). The periodic EFSM is a kind of a real-time extension of the EFSM model that after some constant period T has elapsed, it returns to its initial state. In the proposed method, the concurrent periodic EFSMs are translated into a single periodic EFSM on-the-fly, and the parameter condition is derived. The parameter condition WPC(s,f), in order that the state s satisfies the property f, is derived by recursively computing the subconditions WPC(s_i, f_i) for its next states s_i and their derived properties f_i. We also introduce some optimization heuristics, such as the quantifier elimination of the derived formula. |
| Keyword(in Japanese) | (See Japanese page) |
| Keyword(in English) | parametric model checking / real-time systems / periodic EFSMs / temporal logic / quantifier elimination |
| Paper # | DC2002-41 |
| Date of Issue |
| Conference Information | |
| Committee | DC |
|---|---|
| Conference Date | 2002/11/21(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 | Dependable Computing (DC) |
|---|---|
| Language | JPN |
| Title (in Japanese) | (See Japanese page) |
| Sub Title (in Japanese) | (See Japanese page) |
| Title (in English) | Parametric Model Checking of Concurrent Periodic EFSMs and an Efficient Simplification Method of Parameter Conditions |
| Sub Title (in English) | |
| Keyword(1) | parametric model checking |
| Keyword(2) | real-time systems |
| Keyword(3) | periodic EFSMs |
| Keyword(4) | temporal logic |
| Keyword(5) | quantifier elimination |
| 1st Author's Name | Fumihiko MASUDA |
| 1st Author's Affiliation | Graduate School of Engineering Science and Technology, Osaka University() |
| 2nd Author's Name | Takanori MORI |
| 2nd Author's Affiliation | Graduate School of Engineering Science and Technology, Osaka University |
| 3rd Author's Name | Akio NAKATA |
| 3rd Author's Affiliation | Graduate School of Information Science and Technology, Osaka University |
| 4th Author's Name | Teruo HIGASHINO |
| 4th Author's Affiliation | Graduate School of Information Science and Technology, Osaka University |
| Date | 2002/11/21 |
| Paper # | DC2002-41 |
| Volume (vol) | vol.102 |
| Number (no) | 479 |
| Page | pp.pp.- |
| #Pages | 6 |
| Date of Issue | |