Basic Research on the logical semantics of agent calculi based on concurrent process calculi
| Project/Area Number |
10680347
|
|---|
| Research Category |
Grant-in-Aid for Scientific Research (C)
|
| Allocation Type | Single-year Grants |
|---|
| Section | 一般 |
|---|
| Research Field |
計算機科学
|
|---|
| Research Institution | SHIZUOKA UNIVERSITY |
|---|
Principal Investigator |
TOGASHI Atsushi Shizuoka University, Professor, 情報学部, 教授 (20172140)
|
|---|
| Co-Investigator(Kenkyū-buntansha) |
和泉 憲明 静岡大学, 情報学部, 助手 (50293593)
|
|---|
| Project Period (FY) |
1998 – 1999
|
| Project Status |
Completed (Fiscal Year 1999)
|
| Budget Amount *help |
¥2,900,000 (Direct Cost: ¥2,900,000)
Fiscal Year 1999: ¥1,100,000 (Direct Cost: ¥1,100,000)
Fiscal Year 1998: ¥1,800,000 (Direct Cost: ¥1,800,000)
|
|---|
| Keywords | higher order process calculus / operational semantics / computation model / higher order modal logic / type system / higher order programming language / equivalence / interpretor |
|---|
| Research Abstract |
The main objectives of this research are as follows:
(1) We propose a computational model of higher order concurrent processes and establish their theoretical operational semantics.
(2) Based on the foundations we implement a programming environment and apply it to several practical examples.
We have obtained the following results:
(1) Contraction of a Higher Order Process Calculus
We have proposed a higher order process calculus to describe concurrent systems rigorously. This calculus gives mathematical foundations of the following research items (2) and (3).
(2) Establishment of Mathematical Foundations on Operational Semantics of Higher Order Processes
For the computational calculus proposed in (1), we have carried out the following items with their results:
(a) Equivalence of Processes:
We have given a theory on equivalence of higher order processes based on their operational semantics.
(b) Higher Order Modal System and Model Checking:
We have proposed a proof system for the higher order process calculus and given the theorems on soundness and completeness. A mechanical model checking method for the system have been given as well.
(c) A Type System:
We have given a type system for the calculus and discussed its properties.
(3) Development of Programming Environment
We have implemented the programming environment for the calculus and applied it to several practical examples.
|
Report
(3 results)
Research Products
(33 results)
