| Project/Area Number |
15K15969
|
|---|
| Research Category |
Grant-in-Aid for Young Scientists (B)
|
| Allocation Type | Multi-year Fund |
|---|
| Research Field |
Software
|
|---|
| Research Institution | Tokyo Institute of Technology |
|---|
Principal Investigator |
|
|---|
| Project Period (FY) |
2015-04-01 – 2019-03-31
|
| Project Status |
Completed (Fiscal Year 2018)
|
| Budget Amount *help |
¥3,770,000 (Direct Cost: ¥2,900,000、Indirect Cost: ¥870,000)
Fiscal Year 2017: ¥1,300,000 (Direct Cost: ¥1,000,000、Indirect Cost: ¥300,000)
Fiscal Year 2016: ¥1,170,000 (Direct Cost: ¥900,000、Indirect Cost: ¥270,000)
Fiscal Year 2015: ¥1,300,000 (Direct Cost: ¥1,000,000、Indirect Cost: ¥300,000)
|
|---|
| Keywords | リアクティブシステム仕様 / 実現可能性 / ω-オートマトン / ωオートマトン |
|---|
| Outline of Final Research Achievements |
Realizability verification of reactive system specifications can detect dangerous situations that may arise that were not expected while drawing up the specifications. However, such verification typically involves complex, intricate analyses. In this research, we aimed at reducing the cost of realizability verification for reactive system specifications, and we worked on the following: (1) We developed an efficient method (called partially symbolic method) for implementing procedures of realizability verification, in which binary decision diagrams (BDDs) are used partially. The greatest feature of this method is that it is applicable to realizability verification without approximation (2) We developed an on-the-fly simplification method for omega-automata which are used in realizability verification.
|
| Academic Significance and Societal Importance of the Research Achievements |
本研究の意義は，リアクティブシステム仕様の非近似的な実現可能性判定の効率化に成功した点である．既存研究では，シンボリック技法を適用するために近似的なアプローチがとられていた．本研究では，部分シンボリック技法により非近似的な実現可能性判定手続きを効率的に実装する手法を提案し，実験により，近似的なアプローチに引けを取らない性能がでることを確認した．
|
