| 研究概要 |
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で用いられている手法を一階へ拡張して証明した．
|
