1995 Fiscal Year Annual Research Report
| Project/Area Number |
07680341
|
|---|
| Research Category |
Grant-in-Aid for General Scientific Research (C)
|
| Research Institution | Tokyo Institute of Technology |
|---|
Principal Investigator |
米崎 直樹 東京工業大学, 大学院・情報理工学研究科, 教授 (00126286)
|
|---|
| Co-Investigator(Kenkyū-buntansha) |
友石 正彦 東京工業大学, 大学院・情報理工学研究科, 助手 (60262284)
|
|---|
| Keywords | 実時間ソフトウェア / 仕様記述 / 検証方式 / 時間論理 / 実時間論理 |
|---|
| Research Abstract |
平成8年度の研究結果は、以下の三つの成果にまとめられる。
・実時間論理の研究
実時間システムの検証に適した実時間論理の構築のために、様々な実時間論理を比較検討し、新しい実時間論理RTLを定義した。この言語は単純な時間様相しか持たないが、十分な記述力を持っている。この言語について稠密時間のモデルを許す場合、本質的にどのような要素が決定可能性に影響を与えるかについて検討し、決定可能性を保持するための必要条件について研究を行なった。また、到達可能な部分集合についてその決定手続きを与え、さらにその公理化可能性についても検討を行なった結果、強完全な公理化が行なえないことが判明した。
・リアクティブシステムの検証の研究
リアクティブシステムの仕様記述の途中段階において、その無矛盾性、実現可能性等を判定するときには、それまでに検証された部分の情報を再利用出来ることが望ましい。そこで仕様の追加、削除に応じた段階的検証方法について研究を行ない、そこで用いられるタブロ-の新しいデータ構造を与えた。また、リアクティブシステムの実現可能性について研究を行ない、実現可能でない仕様については、それを実現可能とするための外部環境制約式を求める方法を与えた。
・非標準論理の証明方法の研究
様相論理の一般的証明方法である様相記号列の統一化における失敗情報を証明戦略に応用する方法について研究を行なった。この方法は実時間論理の証明に対しても拡張されるよう考えられている。また、資源を共有する並行システムの検証に有用な線形論理についても研究を行ない、その自動証明法を与えた。
|
-
[Publications] 米崎直樹,鈴木康人,須藤忠祐: "実時間論理RTL" 日本ソフトウェア科学会第12回大会論文集. 137-140 (1995)
-
[Publications] Miyoko Kawamura,Naoki Yonezaki: "Non Clausal Linear Resolution for Propositional Linear Logic" Information Modelling and Knowledge Bases. VI. 215-229 (1995)
-
[Publications] 三木一秀,友石正彦、米崎直樹: "リアクティブシステム仕様の段階的記述プロセスに対応した検証法" 日本ソフトウェア科学会第12回大会論文集. 141-144 (1995)
-
[Publications] 森亮靖、米崎直樹: "実時間論理によるリアクティブシステム仕様の外部イベント制約式" 日本ソフトウェア科学会第12回大会論文集. 177-180 (1995)
-
[Publications] 南沢吉昭、米崎直樹: "導出法による線形論理CLLeの自動証明戦略" 情報処理学会第50回全国大会講演論文集. 3-3-3-4 (1995)
-
[Publications] 萩原茂樹、米崎直樹: "様相論理証明における失敗情報の利用" 日本ソフトウェア科学会第12回大会論文集. 105-108 (1995)
