文献

J-GLOBAL ID：201202243473591887   整理番号：12A1663252

多重Ambient Calculusによる物流記述に対する弱双模倣等価性を用いたモデル検査

Model Checking for Freight Systems Written in the Multiple Ambient Calculus Using Weak Bisimulation

著者 (3件)： 樋口昌宏 (近畿大) ,  森田哲平 (近畿大) ,  加藤暢 (近畿大)
資料名： 情報処理学会論文誌トランザクション(CD-ROM)  (情報処理学会論文誌 Computer Vision and Applications(CD-ROM))
巻： 2012  号： 1  ページ： ROMBUNNO.PUROGURAMINGU,VOL.5,NO.3,50-60  発行年： 2012年10月15日 
JST資料番号： L7379A  ISSN： 1882-7772  資料種別： 逐次刊行物 (A)
記事区分： 原著論文  発行国： 日本 (JPN)  言語： 日本語 (JA)

抄録/ポイント： 我々はAmbient Calculus(AC)による物流システムの記述とそのモデル検査に関する研究を進めている。モデル検査において数千個規模の貨物輸送を扱おうとすると,プロセス式が巨大かつ複雑なものとなるため,状態空間爆発がおこり検証が実際上不可能になるという問題がある。これに対処するため,我々は個々の貨物の取扱いを個別のプロセス式として記述することが可能な多重AmbientCalculus(MAC)を提案し,プロセス式間の弱双模倣等価関係を導入し,その性質について議論した。本論文では,MACにより記述された物流システムのモデル検査法を提案し,それに基づくモデル検査システムについて述べる。提案する検査法では,多数の貨物に対する輸送計画を記述した式Pが,ある貨物cの輸送に関する所期の性質f(c)を満たしていることの検証を,貨物cに対する輸送計画を含むより小規模な式Qを用いて以下の2つの性質の検証に帰着させる。(i)PとQが貨物cの輸送について弱双模倣等価である(振舞いが等しい)こと,(ii)Qがf(c)を満たすこと。本論文では,この手法に基づくモデル検査システムの構築,ならびに検証実験についても述べる。(著者抄録)

シソーラス用語： *モデル検査 ,  計算モデル ,  *物流システム ,  貨物 ,  組合せ問題 ,  輸送計画 ,  小規模 ,  式 ,  シミュレーション ,  等価性 ,  *プログラム実行 ,  実験
準シソーラス用語： Ambient Calculus ,  状態空間爆発 ,  状態爆発問題 ,  数式 ,  バイシミュレーション ,  検証実験

分類 (3件)： 計算理論  (JB02000A) ,  物的流通  (KA08000O) ,  計算機システム開発  (JD02010R)

引用文献 (11件)：

• [1] 日本経済新聞社:海上コンテナの位置追跡,日本経済新聞2007年1月24日発行夕刊3面(2007).
• [2] 国土交通省:「メコン地域陸路実用化走行試験」-インドシナ半島物流を変える陸路物流の実用化へのチャレンジ,入手先〈http://www.mlit.gojp/kisha/kisha07/15/151018_.html〉.
• [3] 国土交通省:米国国土安全保障省及び国土交通省による海上貨物追跡タグシステム(MATTS)の通信能力実証実験,入手先〈http://www.mlit.g0jp/kisha/kisha07/11/110427_.html〉.
• [4] Cardelli, L. and Gordon, A.D.: Mobile Ambients, Theo-retical Computer Science, Vo1.240, pp.177-213(2000).
• [5] 森本大輔,加藤暢,樋口昌宏:AmbientCalculusを用いた物流検査システム,情報処理学会論文誌:プログラミン,Vbl.48,No.SIG10(PRO33),pp.151-164(2007).

タイトルに関連する用語 (5件)： 多重 ,  物流 ,  記述 ,  双模倣等価性 ,  モデル検査