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
|
| Project Status |
Completed (Fiscal Year 2013)
|
| Budget Amount *help |
¥5,070,000 (Direct Cost: ¥3,900,000、Indirect Cost: ¥1,170,000)
Fiscal Year 2013: ¥1,690,000 (Direct Cost: ¥1,300,000、Indirect Cost: ¥390,000)
Fiscal Year 2012: ¥1,560,000 (Direct Cost: ¥1,200,000、Indirect Cost: ¥360,000)
Fiscal Year 2011: ¥1,820,000 (Direct Cost: ¥1,400,000、Indirect Cost: ¥420,000)
|
|---|
| 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.
|
Report
(4 results)
Research Products
(6 results)
