2011 Fiscal Year Annual Research Report
時間概念を導入したAmbient Calculusによる物流システムの記述
| Project/Area Number |
22500040
|
|---|
| Research Institution | Kinki University |
|---|
Principal Investigator |
樋口 昌宏 近畿大学, 理工学部, 准教授 (00238289)
|
|---|
| Keywords | プロセス代数 / 時間制約 / 弱双模倣等価 / モデル検査 / 閉包性 |
|---|
| Research Abstract |
昨年度に引き続いて、物流管理システムの構築への応用を想定し、動的に変化するオブジェクトの階層構造の記述に適したプロセス代数であるAmbient Calculusの拡張に関する研究を進めた。
昨年度定めた時間付きAmbient Calculusの構文規則、遷移規則に基づく直接実行系の実装を進めた。
一方Ambient Calculusないしは時間付きAmbient Calculusで実際の海上物流などの物流システムを記述しようとする場合、取り扱う貨物の数が膨大なものとなるためプロセス式が複雑なものとなってしまう。物流システム記述の正当性確認のためのモデル検査、あるいは記述に基づく物流管理システムの構築を考えると、なるべく単純な構造のプロセス式により物流システムの持つ対称性、並行性を適切に表現することが重要になる。そこで本研究では、単純な構造での大規模プロセス式の記述を可能とするため、Ambient Calculusの拡張として、複数のプロセス式の組で物流システムを表現する多重Ambient Calculusを提案した。さらに多重Ambient Calculusのプロセス式間の等価関係として弱双模倣関係に着目し、この関係がプロセス式の追加操作について閉じているなどのいくつかの性質を示した。さらに弱双模倣等価性を活用して、多数の貨物を扱う物流システムの正当性確認のためのモデル検査を、より少数の貨物のモデル検査と、それらの間の弱双模倣等価関係の確認に帰着する方法を考案した。さらに考案した方法に基づくモデル検査システムを実装し、検証実験によりその有効性を確認した。
|
| Current Status of Research Progress |
Current Status of Research Progress
2: Research has progressed on the whole more than it was originally planned.
Reason
当初の計画はAmbient Calculusに時間概念を導入することであったが、物流システムへの適用を想定した場合大規模な物流計画を適切に記述することが重要になることに鑑み、本年度は大規模物流計画の取扱いがより容易になる多重Ambient Calculusを導入し、その理論的性質を示し、モデル検査技法の検討を行った。当初の予定とは研究の方向が若干異なっているものの、ほぼ想定通りの成果をあげているといってよい。
|
| Strategy for Future Research Activity |
次年度は多重Ambient Calculusへの時間概念の導入について考察する。
まず構文規則、遷移規則の定義から始め、理論的性質の解明、物流計画記述、物流検査システムの構築方法の考察、効率的なモデル検査技法の検討を進めていく。
|
