2011 Fiscal Year Annual Research Report
形式手法のための論理の構築と、一階拡張が満たす性質に関する研究
| Project/Area Number |
22500021
|
|---|
| Research Institution | Sendai National College of Technology |
|---|
Principal Investigator |
岡本 圭史 仙台高等専門学校, 総合科学系, 准教授 (00308214)
|
|---|
| Co-Investigator(Kenkyū-buntansha) |
北村 崇師 産業技術総合研究所, セキュアシステム研究部門, 研究員 (70530484)
|
|---|
| Keywords | 形式手法 / 論理 / 命題様相μ計算 / 一階様相μ計算 / モデル / (論理の)表現力 |
|---|
| Research Abstract |
1.検証のための新しい論理の構築:物流システムの分析・検証のための論理の構築を行った.本研究では,配達システムにおける荷物配達要求記述言(DR-SLL:Delivery Requirements Specification Language)を時相論理であるLTLを基に構築した.さらに,この物流システム検証のためのシステムを,既存のLTL処理機を用いて実装するために,DRSLのLTLへの変換規則を考案した.(北村は関連成果で,2011年度山下記念研究賞を受賞)
2.A.モデル理論: "一般モデルで充足可能な命題様相μ計算の論理式は,標準モデルでも充足可能か?"という問題を解決することがこの項目の目標である.昨年度の成果である「与えられた有限な一般モデルに対し,それと論理式の真偽に関して等価な標準モデルの構築」に関する研究を継続した.有限という制約を外すことができるか否かは解決できていない.
2.B.表現力:昨年度の結果は,1)FOCTL*の表現力がFOM-muの表現力よりも弱いことを,論理式の構成に関する帰納法で証明し,さらに,2)後者の論理式で前者の論理式と等価にならないものを具体的に示すという二段階からなる.2)の方針を他の一階時相論理達の表現力比較にも適用できるよう,具体的な論理式を探すことが必要であり,命題時相論理の表現力比較で用いられる手法を調査し,その結果をまとめた.これらの結果を一階時相論理の表現力比較へ応用することで,一階時相論理達の表現力の差を示すことができると考えられるが,証明は完成していない.一階様相μ計算と似た論理を経由することで命題様相μ計算のモデル検査の効率を上げる研究などがある.一階様相μ計算の部分論理である一階時相論理達の表現力を明らかにすることで,記述能力・計算量の観点から,形式的検証などで利用する際に適切な論理を選択出来るようになる.
|
| Current Status of Research Progress |
Current Status of Research Progress
2: Research has progressed on the whole more than it was originally planned.
Reason
(1)本年度以前からの成果を発展させることでスムースな研究展開ができたためと考えられるため.(2.A).命題様相μ計算の完全性証明は困難であり,それと等価な箇所が本年度以降に残ったと考えられるため.(2.B)昨年度の成果を用いて,他の一階時相論理たちの表現力の大小関係を示すことができると考えられ,本年度の調査結果を用いて,大小関係が真の大小関係となることを証明可能であると考えられるため.
|
| Strategy for Future Research Activity |
1.本年度構築した論理のブラッシュアップ及び,提案した論理を用いた検証例の有用性に関する研究を推進する.
2. A.Finite Model Propertyの成り立つ条件を精査し,無限モデルから有限モデルへの対応をつけることで,無限モデルと有限モデルのギャップを埋めることができるか否かを検討する.また,従来の完全性定理の証明で用いられているアイディアをモデル理論への移植可能性を検討する.
2. B.昨年度に定式化した一階時相論理用に拡張された論理式に関する帰納法を用いて,ある一階時相論理の表現力が別の一階時相論理の表現力より弱いことを示す.また,本年度調査した命題時相論理の表現力比較の手法を拡張し,ある一階時相論理の表現力が別の一階時相論理の表現力より弱くないことを示す.
|
