1997 Fiscal Year Annual Research Report
| Project/Area Number |
07680341
|
|---|
| Research Institution | Tokyo Institute of Technology |
|---|
Principal Investigator |
米崎 直樹 東京工業大学, 大学院・情報理工学研究科, 教授 (00126286)
|
|---|
| Co-Investigator(Kenkyū-buntansha) |
友石 正彦 東京工業大学, 大学院・情報理工学研究科, 助手 (60262284)
|
|---|
| Keywords | 実時間ソフトウェア / 仕様記述 / 検証方式 / 時間論理 / 実時間論理 / 線形論理 / 適切さの論理 |
|---|
| Research Abstract |
以下の各項目につき研究成果を得た。
1.時間領域の違いによる証明体系の研究
離散性を持つ体系に対する、結合法をベースとした様相記号列の統一化による証明方法を考案した。この方法では、統一化に自己代入を許すとともに、式の無限個の複製を表す記号を導入した。また、すでに提案した実時間システムの検証を目的する実時間を記述可能な論理RTLを基にし、RTLの意味論を保存して有理数時間に制限したRTL^Qについて公理系を提案し、その弱完全性の証明方法について研究を行った。
2.線型論理の意味論に関する研究
様相演算子まで含む命題線形論理CLL_eに対し、モデルを基にした、直感的にわかりやすい意味論を与えた。式を命題の要求と供給と見ることで原始命題の収支に着目し、この収支をモデルで表現した。このモデルでは、様相演算子はその式が無限にあることを表現している。そしてモデルと式との間の命題の収支を計算することで、式に真偽値を割り当てている。
3.発展的検証方法に関する研究
新たな構造を持ったタブローグラフとその構成方法を導入することで、部分仕様について検証済みの情報を全体仕様の検証に再利用可能なタブロ-法を提案した。特に、線形離散時間フレームにおけるモデルチェッキングの手続きにおいてグラフ生成とは別に必要な「イベンチャリティを確認する手続き」の代わりに、確認した結果の情報も反映したタブローグラフを直接構成可能な構造を与えた。
4.仕様からの適切な情報を推論する論理体系に関する研究
仕様として記述された論理式から、人間にとって意味ある式のみを演繹することは、仕様を検査し過ちを発見しやすくするために重要である。このためにすでに結合子の適切さを考慮した新しい論理ERを構築していたが、本年はこの体系を基に結合子の適切さも考慮した体系LRCを構築し、その性質について論じた。
5.仕様の分類とその判定方法に関する研究
リアクティブシステムの仕様記述について、その実現可能性に至るいくつかのクラスを分類しその性質について論じた。このクラス分けは、欠陥のある仕様を実現可能な仕様に修正してゆく過程において、仕様記述者に対して、より詳細な情報を与える。また、仕様がそのクラスに属するか否かに関する判定アルゴリズムをその正しさの証明とともに与えた。
|
Research Products
(6 results)
-
[Publications] 森亮靖、友石正彦、米崎直樹: "時相論理によるリアクティブシステム仕様の実現可能性に関する分類" 日本ソフトウェア科学会論文誌(採録決定). (1997)
-
[Publications] Yoshiaki Minamisawa, Masahiko Tomoishi and Naoki Yonezaki: "A New semantics for Linear Logic and its Completeness" Information modeling and knowledge bases. VIII. 155-166 (1997)
-
[Publications] Shigeki Hagihara and Naoki Yonezaki: "A Connection based proof method for Modal logic restricted to Discrete frames" Poster Session Abstracts,Fifteenth International Joint Conference on Artificial Intelligence. 43-43 (1997)
-
[Publications] 友石正彦、米崎直樹: "合成可能な時間論理タブロ-の構成法" 電子情報通信学会技術研究報告97. 390. 17-22 (1997)
-
[Publications] 須藤忠祐、米崎直樹: "実時間論理RTL^Qの公理化に関する研究" 日本ソフトウェア科学会第14回大会論文集. 381-384 (1997)
-
[Publications] 南澤吉昭、米崎直樹: "線形論理CLL_eのモデルを用いた意味論" 情報処理学会第55回全国大会論文集(2). 547-548 (1997)
