文献

J-GLOBAL ID：201702276094286186   整理番号：17A1041376

時間付きオートマトンの境界モデル検査のための効率的符号化

Efficient encoding for bounded model checking of timed automata

著者 (5件)： Chen Zuxi (School of Computer Science and Technology, Huaqiao University, Xiamen 361021, China) ,  Xu Zhongwei (School of Electrical and Electronic Engineering, Tongji University, Shanghai 201804, China) ,  Du Junwei (School of Information of Science and Technology, Qingdao University of Science and Technology, Qingdao, Shangdong 266061, China) ,  Mei Meng (School of Electrical and Electronic Engineering, Tongji University, Shanghai 201804, China) ,  Guo Jing (School of Electrical and Electronic Engineering, Tongji University, Shanghai 201804, China)
資料名： IEEJ Transactions on Electrical and Electronic Engineering  (IEEJ Transactions on Electrical and Electronic Engineering)
巻： 12  号： 5  ページ： 710-720  発行年： 2017年09月 
JST資料番号： W1854A  ISSN： 1931-4973  資料種別： 逐次刊行物 (A)
記事区分： 原著論文  発行国： アメリカ合衆国 (USA)  言語： 英語 (EN)

抄録/ポイント： 時間付きオートマトンの境界モデル検査(BMC)はコンカレント実時間システムの立証に成功裏に適用されてきたが,これは結果として得られた定式の満足度を解くための大規模検索空間と同様,反例,BMC定式を解くために使用される決定手順の効率を見い出すために必要とされる大規模境界に今なお制限されている。本論文では,上述した三つの問題すべてに取り組むための系統的符号化方式を示す。最初の問題に取り組むために,最初に時間経過を特徴づけるために使用されるBMCステップを削るための構成遷移として,時間遅延に続く離散動作を符号化する。次により独立した動作が並列実行できる局所時間時間セマンティックスを活用する。これはBMCステップの必要数をさらに低減し,それゆえに定式のサイズをも低減する。より効率的な決定手順を使用するために,時間付きオートマトンの線形算術符号化を満足度モジュロ理論ソルバでより効率的に解ける差分論理定式へ変換する。最後の問題に取り組むために,いくつかの有効な遷移の実行の陽的状態部分的次元低減の考えを使用し,いくつかの冗長マルチステップ実行を除去する,それゆえに探索空間を制限するために付加的制約を加える。実験結果によって,本符号化がこれまでの符号化より著しく優れていることを示す。Copyright 2017 Wiley Publishing Japan K.K. All Rights reserved. Translated from English into Japanese by JST.

シソーラス用語： *オートマトン ,  *時間依存性 ,  *モデル検査 ,  システム ,  次元縮小 ,  意味論 ,  *符号化 ,  オートマトン理論 ,  相互排除 ,  プロトコル ,  定理証明
準シソーラス用語： *時間付きオートマトン ,  *境界モデル検査 ,  実時間システム ,  セマンティックス ,  算術符号化 ,  反例

著者キーワード (4件)： bounded model checking ,  real-time systems ,  timed automata ,  satisfiability modulo theories

分類 (1件)： オートマトン理論  (JB04000O)

引用文献 (21件)：

• Audemard G, Cimatti A, Kornilowicz A, Sebastiani R. Bounded model checking for timed systems. Proceedings of the 22nd IFIP WG 6.1 International Conference on Formal Techniques for Networked and Distributed Systems, Houston, London, UK, UK FORTE '02. Springer-Verlag: 2002; 243-259.
• Sorea M. Bounded model checking for timed automata. Electronic Notes in Theoretical Computer Science 2002. Elsevier: 2002.
• Niebert P, Mahfoudh M, Asarin E, Bozga M, Maler O, Jain N. Verification of timed automata via satisfiability checking. Formal Techniques in Real-Time and Fault-Tolerant Systems . Damm W, d. Olderog E-R (eds). Springer: Berlin, Heidelberg; 2002; 225-243.
• Miller C, Gitina K, Scholl C, Becker B. Bounded model checking of incomplete networks of timed automata. 2010 11th International Workshop on Microprocessor Test and Verification (MTV), December, 2010; 61-66.
• Kindermann R, Junttila T, Niemelä I. Beyond lassos: complete smt-based bounded model checking for timed automata. Formal Techniques for Distributed Systems. Giese H, Rosu G (eds). Springer: Berlin, Heidelberg; 2012; 84-100.

タイトルに関連する用語 (3件)： 時間付きオートマトン ,  境界モデル検査 ,  符号化