2013 Fiscal Year Final Research Report
Improvement of liveness model checking performance degraded by obese formulas
| Project/Area Number |
23500041
|
|---|
| Research Category |
Grant-in-Aid for Scientific Research (C)
|
| Allocation Type | Multi-year Fund |
|---|
| Section | 一般 |
|---|
| Research Field |
Software
|
|---|
| Research Institution | Japan Advanced Institute of Science and Technology |
|---|
Principal Investigator |
OGATA KAZUHIRO 北陸先端科学技術大学院大学, 情報科学研究科, 准教授 (30272991)
|
|---|
| Project Period (FY) |
2011 – 2013
|
| Keywords | モデル検査 / 活性 / 公平性 / 準公平性 / 分割統治 / 公平性の理解 / 反例 / Maude |
|---|
| Research Abstract |
Model checking a liveness property lprop under a fairness assumption fair, the formula is in the form "fair => lprop". The formula is transformed into a Buchi automaton. The transformation requires an exponential time and space of the size of the formula. If the formula becomes large, it becomes (almost) impossible to transform the formula into a Buchi automaton and then to model check the formula. The research proposes a way of making the model checking feasible by model checking "fair => qfair" and "qfair => lprop" for some formula qfair such that the size of qfair is (much) smaller than that of fair.
|
