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