2012 Fiscal Year Annual Research Report
時間概念を導入したＡｍｂｉｅｎｔ Ｃａｌｃｕｌｕｓによる物流システムの記述
| Project/Area Number |
22500040
|
|---|
| Research Institution | Kinki University |
|---|
Principal Investigator |
樋口 昌宏 近畿大学, 理工学部, 准教授 (00238289)
|
|---|
| Project Period (FY) |
2010-04-01 – 2013-03-31
|
| Keywords | プロセス代数 / 時間制約 / タイムアウト / モデル検査 / 弱双模倣等価 |
|---|
| Research Abstract |
一昨年度、昨年度に引続いて、物流監視システムの構築への応用を想定し，動的に変化するオブジェクトの階層構造を記述するためのプロセス代数であるAmbient Calculusの拡張に関する研究を進めた。 主として一昨年度に検討した時間付きAmbient Calculus の構文規則、遷移規則の策定については、一昨年度の提案を大幅に見直し、指定した時間内に指定した動作が行われなかったことを表す特別なアンビアントを導入し、さらに通信を含む動作にも対応するような，構文規則、遷移規則を与えた。また、タイムアウト動作や、指定した時間以内に実行しなければならない動作を簡潔に記述するためのマクロ構文を与え、それらを用いて海上物流や交通信号などのシステムの記述を行い、良好な記述性を確認した。 また、主として昨年度検討した多重Ambient Calculusについては，多重Ambient Calculusで記述した物流計画が所期の性質を満たしていることを確認するモデル検査法について検討を進めた。具体的には、まず多重Ambient Calculus による物流計画に対するモデル検査システムのための公理系の策定した。次に、多数のコンテナを運ぶような大規模な物流計画のモデル検査を，少数のコンテナを運ぶ物流計画のモデルに対する検査に帰着させるための弱双模倣等価関係を用いた検証法を考案した。また、考案した手法に基づいて多重AmbientCalculus のプロセス式間の弱双模倣等価性を検証するシステムの構築，そしてそれらの成果を利用したモデル検査システムの構築および実証実験を行った。実験の結果、貨物の種類が数種程度であれば、その数がいくつであっても、一般的なPCで数十秒で物流計画の正当性が検証できることを確認した。
|
| Current Status of Research Progress |
Reason
24年度が最終年度であるため、記入しない。
|
| Strategy for Future Research Activity |
24年度が最終年度であるため、記入しない。
|
