1999 Fiscal Year Annual Research Report
並行計算に基づくエージェント計算系の論理的意味論に関する基礎研究
Project/Area Number |
10680347
|
Research Institution | SHIZUOKA UNIVERSITY |
Principal Investigator |
富樫 敦 静岡大学, 情報学部, 教授 (20172140)
|
Keywords | 高階並行プロセス計算 / 動作的意味論 / 計算モデル / 高階様相論理 / タイプシステム / 高階並行プログラミング言語 / 等価性 / 言語処理系 |
Research Abstract |
本研究の目的は,知的エージェントの数学的計算モデルを構築し,その論理的動作意味論に関する基礎理論を確立することである.具体的な研究実施項目と内容を以下に記す. (1)エージェントのための計算モデルの構築 (2)エージェント計算の論理的意味論に関する数学的基礎理論の確立 (3)エージェント言語の開発 (4)モデル検証システムの実装 本年度は,以下の項目に関して,以下の成果を得た. (2b)モデル検証方法・システムの理論的構築 (2a)のベース論理に基づき,エージェントの論理的性質を検証するために,以下の3種類の検証方法・システムについて検討した. 演繹的手法:Gentzenのsequent計算風の合成性(compositionality)を有する証明システム.変換的手法:充足可能性に関して必要十分性を備えた論理式に変換し,充足可能であることとその論理式が真となることが等価であるような変換法.タブロー的手法:一般に,演繹システムを逆向き(トップダウン的)に用いるとタブロー的証明システムになるが,この小項目ではプロセスの構造によって定まる遷移関係に着目し,遷移関係に依存したシンボリックな証明システムを提案する. (3)エージェント言語の開発 (4)モデル検証システムの実装 (3)と(4)は,(1),(2)の成果に基づき,エージェント言語の開発と論理的意味をチェックするためのモデル検証システムを,初年度新設設備のスパークステーション上にjavaを用いて実装した.実装したシステムは,Web上に公開した.
|
Research Products
(7 results)
-
[Publications] Shigetomo Kimura,Atsushi Togashi,Norio Shiratori: "Inductive Synthesis of Recursive Processes from Logical Properties"Information and Computation. (掲載予定). (200-)
-
[Publications] Fumiaki Kanezashi,Xiaosong Lu,Atsushi Togashi: "M-pi calculus : A calculus for module description"Proc.of the International Workshop on Principle of Software Evolution'99. 65-69 (1999)
-
[Publications] Xiaosong Lu,Fumiaki Kanezashi,Atsushi Togashi: "Hierarchical Specification of Reactive System Requirements"Proc.of the 13th International Conference on Information Networking. 10B-3.1-10B-3.6 (1999)
-
[Publications] 金指文明,富樫敦: "システム要求からの形式仕様の導出方法"情報処理学会論文誌. 第40巻第1号. 310-321 (1999)
-
[Publications] 金指文明,富樫敦: "M-pi計算:モジュール記述を持つ計算体系"情報処理学会DICOM'99シンポジウム論文集. 43-48 (1999)
-
[Publications] 金指文明,塚崎悟,富樫敦: "Field Walker:プロセス計算に基づく移動型エージェントシステム-Javaによる実装-(ベストプレゼンテーション賞受賞)"情報処理学会DICOM'99シンポジウム論文集. 37-42 (1999)
-
[Publications] 金指文明,塚崎悟,富樫敦: "Field Walker:プロセス計算に基づく分散プログラミングシステム"ソフトウェア工学の基礎VI,レクチャーノート/ソフトウェア工学22,日本ソフトウェア科学会FOSE'99. 28-35 (1999)