|
JAIST Repository >
School of Information Science >
Grants-in-aid for Scientific Research Papers >
FY 2013 >
Please use this identifier to cite or link to this item:
https://hdl.handle.net/10119/12176
|
| Title: | 論理式肥大に伴う活性のモデル検査の非効率化の改善 |
| Other Titles: | Improvement of liveness model checking performance degraded by obese formulas |
| Authors: | 緒方, 和博 |
| Authors(alternative): | Ogata, Kazuhiro |
| Keywords: | モデル検査
活性
公平性
準公平性
分割統治
公平性の理解
反例
Maude |
| Issue Date: | 23-Apr-2014 |
| Abstract: | 公平性のもとでの活性のモデル検査対象の論理式は"公平性 ⇒ 活性"の形をとる。この論理式はBuchiオートマトンへ変換される。この変換は論理式の大きさに対しべき乗の計算と空間を必要とするため、公平性が大きくなるとBuchiオートマトンへの変換が実質不可能になり、モデル検査自体もできなくなる。本研究では、"公平性 ⇒ 準公平性"を満たし、公平性より小さな論理式である準公平性を探し、"準公平性 ⇒ 活性"をモデル検査することで公平性のもとでのモデル検査を可能とする方法を提案する。すなわち、"公平性 ⇒ 活性"の代わりに、"公平性⇒ 準公平性" と"準公平性 ⇒ 活性"をモデル検査することである。 : 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. |
| Description: | 研究種目：基盤研究(C)
研究期間：2011～2013
課題番号：23500041
研究者番号：30272991
研究分野：計算機科学
科研費の分科・細目：ソフトウェア |
| Language: | jpn |
| URI: | https://hdl.handle.net/10119/12176 |
| Appears in Collections: | 2013年度 (FY 2013)
|
Files in This Item:
| File |
Description |
Size | Format |
|---|
| 23500041seika.pdf | | 155Kb | Adobe PDF | View/Open |
|
All items in DSpace are protected by copyright, with all rights reserved.
|
