並列タイトル等Improvement of liveness model checking performance degraded by obese formulas
一般注記公平性のもとでの活性のモデル検査対象の論理式は"公平性 ⇒ 活性"の形をとる。この論理式は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.
研究種目：基盤研究(C)
研究期間：2011～2013
課題番号：23500041
研究者番号：30272991
研究分野：計算機科学
科研費の分科・細目：ソフトウェア
identifier:https://dspace.jaist.ac.jp/dspace/handle/10119/12176
一次資料へのリンクURLhttps://dspace.jaist.ac.jp/dspace/bitstream/10119/12176/1/23500041seika.pdf
連携機関・データベース国立情報学研究所 : 学術機関リポジトリデータベース（IRDB）（機関リポジトリ）
提供元機関・データベース北陸先端科学技術大学院大学 : JAIST学術研究成果リポジトリ