Process algebra based analysis and verification for asynchronous communications appeared in parallel programs
| Project/Area Number |
14540121
|
|---|
| Research Category |
Grant-in-Aid for Scientific Research (C)
|
| Allocation Type | Single-year Grants |
|---|
| Section | 一般 |
|---|
| Research Field |
General mathematics (including Probability theory/Statistical mathematics)
|
|---|
| Research Institution | Ehime University |
|---|
Principal Investigator |
OHTSUKA Hiroshi Ehime University, Faculty of Science, Associate Professor, 理学部, 助教授 (30203839)
|
|---|
| Co-Investigator(Kenkyū-buntansha) |
TSUCHIYA Takuya Ehime University, Faculty of Science, Professor, 理学部, 教授 (00163832)
ISHIKAWA Yasushi Ehime University, Faculty of Science, Associate Professor, 理学部, 助教授 (70202976)
|
|---|
| Project Period (FY) |
2002 – 2004
|
| Project Status |
Completed (Fiscal Year 2004)
|
| Budget Amount *help |
¥2,800,000 (Direct Cost: ¥2,800,000)
Fiscal Year 2004: ¥1,000,000 (Direct Cost: ¥1,000,000)
Fiscal Year 2003: ¥1,000,000 (Direct Cost: ¥1,000,000)
Fiscal Year 2002: ¥800,000 (Direct Cost: ¥800,000)
|
|---|
| Keywords | coordination language / model checking / finite automaton / regular expression / regular expression function / regular expression pattern matching / モデル検証 / プロセス代数 / クリプケ構造 / 失敗集合 / 軌跡 / 可達性解析 |
|---|
| Research Abstract |
In this year, we investigated Knuth-Morris-Pratt type algorithms for regular expression pattern matching problems (called RPM) and for characterize its position and length.
These investigations were derived from our research at the previous years, in which we study parallel programs base on coordination language and tuple space. In this situation, tuple space is modeled by fineite stae machine(FSM) and trace of process is modeled by string or sequence of actions that are primitive operations in coordination language. And we treat some problems in the field of model checking as acceptance problems for FSM or equivalently RPM.
To treat RPM, we adopt regular expression function based on left quotient for strings instead of finite automata approach in order to avoid the "explosion problems for state space" in state based modeling of parallel processes. As a result we constructed algorithms based on regular expression function for solving RPM and for finding the position and length of it in some case of regular expressions.
We presented these results at "Ouyou-suugaku Goudou Kenkyu Syukai" and "The 67^<th> National Convention of IPSJ".
|
Report
(4 results)
Research Products
(1 results)
