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

2000 Fiscal Year Annual Research Report

• Project/Area Number: 12780195
• Research Institution: Tokyo Institute of Technology
• Principal Investigator: 吉浦 紀晃 東京工業大学, 大学院・情報理工学研究科, 助手 (00302969)
• Keywords: 適切さの論理 / 時間論理 / リアクティブシステム / 決定可能性 / 段階的充足可能性 / 実現可能性

Research Abstract

本年度は,本研究においてベースとなる適切さの論理ERの特徴を調べ、また、リアクティブシステムの仕様記述に関する研究を行なった。
・適切さの論理ERが決定可能であることを示し、具体的な決定手続きを構築し、国際会議において発表した。また、ERに関するいくつかの特徴があることを証明した。論理として重要ないくつかの性質が成り立つことが判明したが、同時に、論理では成り立つと考えられているModus ponensやEquivalence Replacementなどのいくつかの性質が成り立たないことも判明した。これらの性質は重要な性質であるが、ある特定の条件においては、ERにおいても成り立つことが判明しているので、この点に関する形式化を行ない、ERが本研究の目的にとって、十分な性質を持つ論理であることを示した。
・リアクティブシステムの仕様記述において、実際にシステムの仕様においては、実現可能性を満たすものはほとんど存在しない。実際のリアクティブシステムは、段階的充足可能性を満たすことが最もあう条件であると考えられる。そのため、仕様の段階的充足可能性の判定手続きと、仕様からのプログラム合成手続きを構築した。そのために、段階的充足可能性が実際のリアクティブシステムの仕様の実現可能性にあたることを示すために、仕様がこの性質を満たすこととSafety Propertyを満たすことの等価性について考察を行なった。
ここで扱っているリアクティブシステムの仕様記述を実例として、支援システムを構築したいと考えている。

Research Products

• [Publications] Noriaki Yoshiura,Naoki Yonezaki: "A Decision Procedure for the Relevant Logic ER"International Conference Tableaux 2000 published in University of St.Andrews Research Report CS/00/01. 109-123 (2000)
• [Publications] Nariaki Yoshiura,Naoki Yonezaki: "Program Synthesis for Stepwise Satisfiable Specification of Reactive System"International Symposium on Princiles of Software Evolution. 58-67 (2000)
• [Publications] 吉浦紀晃,米崎直樹: "リアクティブシステムの段階的充足可能性とSafety Propertyの関係"信学技報. 100・570. 9-16 (2001)