1991 Fiscal Year Final Research Report Summary
Foundamental Study on Fundational Model of Concurrent Computation
| Project/Area Number |
02680020
|
|---|
| Research Category |
Grant-in-Aid for General Scientific Research (C)
|
| Allocation Type | Single-year Grants |
|---|
| Research Field |
Informatics
|
|---|
| Research Institution | Nagoya University |
|---|
Principal Investigator |
SAKABE Toshiki Nagoya Univ., Faculty of Eng., Associate Professor, 工学部, 助教授 (60111829)
|
|---|
| Co-Investigator(Kenkyū-buntansha) |
YUEN Shoji Nagoya Univ., Faculty of Eng., Research Associate, 工学部, 助手 (70230612)
SAKAI Masahiko Nagoya Univ., Faculty of Eng., Research Associate, 工学部, 助手 (50215597)
NAOI Tohru Gifu Univ., Faculty of Eng., Associate Professor, 工学部, 助教授 (10207699)
HIRATA Tomio Nagoya Univ., Faculty of Eng., Associate Professor, 工学部, 助教授 (10144205)
INAGAKI Yasuyoshi Nagoya Univ., Faculty of Eng., Professor, 工学部, 教授 (10023079)
|
|---|
| Project Period (FY) |
1990 – 1991
|
| Keywords | concurrent computation / Functional computation model / CCS / broadcast / narrowing / concurrent process / term rewriting system / dynamic term rewriting calculas |
|---|
| Research Abstract |
The purpose of this research project is to develop a functional model of concurrent computation based on narrowing such that we can analyze and verify concurrent programs by using rewriting techniques.
The results we obtained in the research project are as follows.
We first proposed a computation model called Dynamic Term Rewriting Calculus (DTRC, for short). It is a preliminary version of our target model. DTRC has features such as dynamically changing rewrite rules during computation and hierarchically declaring function symbols, variables and rewrite rules. We obtained fundamental results on confluency and termination of DTRC terms.
We also investigated the theory of process algebras and proposed two extensions of CCS. One is CCS with limit values. It has term rewriting systems as the mechanism for defining (possibly limit) values and has the feature of branching by a limit value. We gave a semantics for the extended CCS by introducing a new concept of test precision. The other extension is CCS with broadcast (called CCS+b). It formalizes broadcast which is characterized with one-to-many communication and nondeterministic communication in receiving signals. We obtained commutativity and associativity lows for choice and parallel composition operators, and expansion low. These lows are useful for analyzing processes.
We studied tree pattern matching and found a parallel algorithm for tree pattern matching which improved the algorithm of Ramesh et al. in time and space.
|
