論理結合子の適切さに基づく有益な情報の導出に関する研究

2003 Fiscal Year Annual Research Report

• Project/Area Number: 15700007
• Research Institution: Gunma University
• Principal Investigator: 吉浦 紀晃 群馬大学, 総合情報処理センター, 助教授 (00302969)
• Keywords: 適切さの論理 / 時間論理 / 仕様検証 / セキュアコンピューティング

Research Abstract

本年度の研究実績の概要として、第一に、論理和、論理積、含意、否定の論理において基本となる論理結合子の出現に、適切さを定義した。さらに、その適切さを反映した論理LRCを提案した。
この適切さは、証明図の構造や推論に利用された知識によって決定される。この論理では、このように定義された論理結合子の適切さを満たす式だけが推論されるという特徴を持つ。このことは、この論理の健全性と完全性を証明することにより言える。つまり、LRCで推論される式は、論理結合子の出現がすべて適切さであり、論理結合子の出現がすべて適切であり推論可能である式は、LRCにより推論されることを証明した。また、LRCと古典論理や適切さの論理の推論の違いを具体例を用いて示し、その有益さを確認した。さらに、LRCの論理学的な特徴を明らかにし、LRCが論理結合子の出現の適切さを反映した論理となっているが、それと引換に、いくつかの典型的な特徴を満たさないことがわかった。
また、研究実績の第二として、リアクティブシステム仕様の検証方法を提案した。この方法では、時間論理で記述されたリアクティブシステム仕様が実現可能であるかどうかを検証し、実現可能でなければ、どの程度、実現可能性から掛け離れているかを調べる。この方法では、仕様の実現可能性の程度は明らかになるが、仕様が実現可能ではない原因を見つけることが出来ない。このような仕様を実現可能なものに変更するために、仕様の修正すべき個所を提示することが必要になる。今回提案した方法は、そのための基礎となる方法であり、前述したLRCなどを利用することにより、仕様の中から修正すべき点を導出する方法を提案することが今後の課題となる。
他の研究実績として、ネットワークを利用した防犯システムの構築があげられる。この研究では、防犯カメラにより撮影された画像データから犯人を見つけることを目的としている。この研究は、本研究課題とは直接は関係しないが、得られた画像データから有益な情報を得るという視点から見ると、本研究とのつながりがあり、今後は、上記2つの実績を利用して、この研究も進める予定である。

Research Products

• [Publications] Noriaki Yoshiura: "Decision Procedures for Several Properties of Reactive System Specification"Lecture Note in Computer Science. (To appear).
• [Publications] Fujii Yusaku, Noriaki Yoshiura, Yoshio Chigara, Katsumasa Hagiwara: "Community Security Platform for Individually Maintained Computers : The e-Vigilante Network Project"Proceedings of IEEE Instrumentation and Measurement Technology Conference 2004. (To appear).
• [Publications] Noriaki Yoshiura: "Logic of Relevant Connectives for Knowledge Base Reasoning"Information Modeling and Knowledge Base. 14. 66-80 (2003)