π計算に対する様相証明システム

• Item type: Trans(1)
• 公開日: 1999-05-15
• タイトル: π計算に対する様相証明システム
• タイトル / 言語: en
• タイトル: A Modal Proof System for π-balculus
• 言語: jpn
• キーワード / 主題Scheme: Other
• キーワード / 主題: 発表概要
• 資源タイプ / 資源タイプ識別子: http://purl.org/coar/resource_type/c_6501
• 資源タイプ: journal article
• 著者所属: 静岡大学情報学部情報科学科
• 著者所属: 静岡大学大学院理工学研究料
• 著者所属(英): en
• 著者所属(英): Department of Computer Science, Shizuoka University
• 著者所属(英): en
• 著者所属(英): Graduate School of Science and Engineering, Shizuoka University
• 著者名: 富樫, 敦; 金指, 文明
• 著者名(英): Atsushi, Togashi; Fumiaki, Kanezashi
• 論文抄録 / 内容記述タイプ: Other
• 論文抄録 / 内容記述: コンピュータシステムのモデルの一つとしてプロセス計算がある. プロセス計算は 数学的なエージェントのモデルであり 形式的にシステムを記述することができる. プロセス計算の代表例として CCS CSP ACP LOTOS π計算がある. このような数学的エージェントのモデルを利用して エージェントを記述することによりそのプロセス式に対しての論理的考察を行なうことができる. 理論的立場から論理的に検証 証明することにより 実際にシステムを構築する際に生じる不具合などを設計の段階から見つけ出すことも可能となる. 本研究では モビリティを持つエージェントのモデルであるπ計算により記述したプロセス式に対しての様相論理に基づいた証明システムNLを提案した. この証明システムNLは π計算から 並行合成演算子を省いた計算体系における証明システムである. この証明システムの健全性と完全性について議論する. また 証明システムの拡張について言及する.
• 論文抄録(英) / 内容記述タイプ: Other
• 論文抄録(英) / 内容記述: To promote rapid development of computer systems, concurrent / parallel processing is one of the promising research items. For the mathematical description for concurrent processes, there have been several proposal as process calculi, formal systems for concurrent processes, such as CCS, CSP, ACP, LOTOS, π-calculus. In this paper, we will propose a modal proof system for the π-calculus, introduced by Milner, Parrow and Walker in 1989. π-calculus is an extension of CCS or CSP, to express mobile agents. Purpose in this paper is to offer a proof system for the π-calculus based on propositional modal logics. A partial soundness and completeness is discussed. An extension of the resulting system is also considered.
• 書誌レコードID / 収録物識別子タイプ: NCID
• 書誌レコードID / 収録物識別子: AA11464814
• 書誌情報: 情報処理学会論文誌プログラミング（PRO）; 巻 40, 号 SIG04(PRO3), p. 67-67, 発行日 1999-05-15
• ISSN / 収録物識別子タイプ: ISSN
• ISSN / 収録物識別子: 1882-7802
• 出版者 / 言語: ja
• 出版者: 情報処理学会