2012 Fiscal Year Annual Research Report
形式手法のための論理の構築と、一階拡張が満たす性質に関する研究
| Project/Area Number |
22500021
|
|---|
| Research Institution | 仙台高等専門学校 |
|---|
Principal Investigator |
岡本 圭史 仙台高等専門学校, 情報システム工学科, 准教授 (00308214)
|
|---|
| Co-Investigator(Kenkyū-buntansha) |
北村 崇師 独立行政法人産業技術総合研究所, セキュアシステム研究部門, 研究員 (70530484)
|
|---|
| Project Period (FY) |
2010-10-20 – 2013-03-31
|
| Keywords | 形式手法 / 論理 / 命題様相μ計算 / 一階様相μ計算 / モデル / (論理の)表現力 |
|---|
| Research Abstract |
1.検証のための新しい論理構築：Milk-run物流システムの分析・検証のための論理の構築及び，その論理の計算機上での実装を行った．本研究では昨年度，Milk-run物流システム複雑性を低減するため，システムの分析・検証の向け論理言語（DR-SL: Delivery Requirements Specification Language）を構築し，さらに，DR-SLから時相論理LTL（Linear Temporal Logic）の変化形への変換規則を考案した．本年度は，時相論理LTLの変化形の意味論を正式に策定し，その意味論に基づき，その変化形の計算機上に実装を行った．この議論とDR-SLからLTLへの変換規則により，DR-SLの計算機上での実行が可能になった．
2.(1)モデル理論：一般モデルと標準モデルの充足性に関しては，モデルが有限であるとうい仮定の下での等価性を過去の共同研究で示した．そこで，無限モデルから有限モデルへの対応をつけるための研究を実施したが，有限という制約を外すことができるか否かは未解決である．
2.(2) 表現力：命題時相論理CTL,LTL,CTL*の一階拡張（一階時相論理）を，それぞれFOCTL,FOLTL,FOCTL*とする．このとき，命題時相論理間の表現力比較と同様の結果が成り立つことを示し，日本数学会2013年度年会等で発表した．具体的には，FOCTL＜FOCLT*，FOLTL＜FOCTL*，FOLTL\nleqslant FLCTL，FOCTL\nleqslant FOLTLが成り立つことを，文献”Sometimes” and ”Not Never” revisited: on branching versus linear time temporal logic, Emerson, Halpernで用いられている手法を一階へ拡張して証明した．
|
| Current Status of Research Progress |
Reason
24年度が最終年度であるため、記入しない。
|
| Strategy for Future Research Activity |
24年度が最終年度であるため、記入しない。
|
