混合型時間アンビアント計算のCTLモデル検査

• Item type: Trans(1)
• 公開日: 2017-11-14
• タイトル: 混合型時間アンビアント計算のCTLモデル検査
• タイトル / 言語: en
• タイトル: CTL Model Checking for Hybrid Timed Ambient Calculus
• 言語: jpn
• キーワード / 主題Scheme: Other
• キーワード / 主題: [発表概要]
• 資源タイプ / 資源タイプ識別子: http://purl.org/coar/resource_type/c_6501
• 資源タイプ: journal article
• 著者所属: 近畿大学
• 著者所属: 近畿大学
• 著者所属: 近畿大学
• 著者所属(英): en
• 著者所属(英): Kindai University
• 著者所属(英): en
• 著者所属(英): Kindai University
• 著者所属(英): en
• 著者所属(英): Kindai University
• 著者名: 稲森, 啓太; 樋口, 昌宏; 加藤, 暢
• 著者名(英): Keita, Inamori; Masahiro, Higuchi; Toru, Kato
• 論文抄録 / 内容記述タイプ: Other
• 論文抄録 / 内容記述: 本発表では混合型時間アンビアント計算（HTAC）を用いて記述した物流システムについてのCTLモデル検査について述べる．HTACとは，アンビアント計算を時間的な制約が記述できるよう拡張したプロセス代数であり，物流システムの持つ動的な階層構造や時間制約を簡潔に表現することができる．HTACを用いて物流システムを記述する際には，物流システムと見なせるための条件をプロセス式が満たしているか確認する必要がある．また，HTACによって物流システムを記述したプロセス式が所期の目的を満たしているかを確認するためには，プロセス式に対してモデル検査を行う必要がある．これらには可達性解析による網羅的な式の列挙が必要であるが，時間制約に関するパラメータが大きいプロセス式を解析する場合，単純な可達性解析では状態空間爆発が起こる．本発表では，この問題を解決するため，式中の時間制約に関するパラメータを変数で表現した式と変数間の関係を表す連立不等式を用いた解析手法を提案する．さらに，提案手法に基づき開発した可達性解析プログラムについても述べる．また本発表では，物流システムが持つHTAC特有の性質を論理式として表現するための時間アンビアント論理を提案し，開発した可達性解析プログラムを利用し構築したプロセス式に対するCTLモデル検査プログラムについても述べる．CTLモデル検査プログラムを用いて行った検査実験の結果についても述べる．
• 論文抄録(英) / 内容記述タイプ: Other
• 論文抄録(英) / 内容記述: In this presentation, we present the CTL model checking method for logistics plans specified in the hybrid timed ambient calculus (HTAC).HTAC is a process algebra as an extension of the ambient calculus and suitable for specifying logistics plans, which contain dynamically changing nested structures and timing constraints.We need to confirm that a HTAC formula satisfies conditions to be regarded as a logistics plan.We also need to perform a CTL model checking for the HTAC formula to ensure that the HTAC formula satisfies desirable properties.Therefore, we have to perform a reachability analysis which enumerates all reachable HTAC formulas.Since a simple reachability analysis for the HTAC formula with large parameters on timing constraints causes a state explosion, we propose an efficient algorithm and developed a reachability analysis program based on it.We also propose the timed ambient logic to express properties of logistics plans specified in HTAC.We developed a CTL model checking program for the HTAC formula using the reachability analysis program.We present checking experiments using the CTL model checking program.
• 書誌レコードID / 収録物識別子タイプ: NCID
• 書誌レコードID / 収録物識別子: AA11464814
• 書誌情報: 情報処理学会論文誌プログラミング（PRO）; 巻 10, 号 5, p. 2-2, 発行日 2017-11-14
• ISSN / 収録物識別子タイプ: ISSN
• ISSN / 収録物識別子: 1882-7802
• 出版者 / 言語: ja
• 出版者: 情報処理学会