文献

J-GLOBAL ID：202002222407876639   整理番号：20A0578655

Booleガードによる時間付きオートマトンのネットワークのパラメータ化モデル検査【JST・京大機械翻訳】

Parameterized model checking of networks of timed automata with Boolean guards

著者 (2件)： Spalazzi Luca (DII, Universita Politecnica delle Marche, Italy) ,  Spegni Francesco (DII, Universita Politecnica delle Marche, Italy)
資料名： Theoretical Computer Science  (Theoretical Computer Science)
巻： 813  ページ： 248-269  発行年： 2020年 
JST資料番号： T0022A  ISSN： 0304-3975  CODEN： TCSDIQ  資料種別： 逐次刊行物 (A)
記事区分： 原著論文  発行国： オランダ (NLD)  言語： 英語 (EN)

抄録/ポイント： パラメータ化モデル検査は,いくつかの仕様が,多くの類似の協調的だが区別できないプロセスから成るシステムに保持されることを検証するための形式的検証技術である。この問題は,到達可能性に制限されても,一般的には決定できないことが知られている。この限界を克服するために,特定のシステムファミリー,論理式あるいはプロセスネットワークのトポロジーに取り組むためのいくつかの技術が探求されている。カットオフの概念,すなわちある特性があるサイズ(カットオフ)までのシステムに対して検証されるならば,それから任意のサイズのシステムに対して検証される。ここでは,近傍が現在どの状態にあるかを見ることにより同期できる任意の数の時間オートマトンからなるネットワークの事例を解析した。著者らは,制御装置として作用する識別プロセスの有無にかかわらず,カットオフがチェックされた式から独立に存在することを示した。ここでは,カットオフを利用して,パラメータ化されたモデル検査問題の複雑さに関する上限を得ることができることを示した。最終的に,著者らは,理論的結果をモデル化するためにどのように使用するかを示し,gossip技術に基づくクロック同期のための分散アルゴリズムを検証する。Copyright 2020 Elsevier B.V., Amsterdam. All rights reserved. Translated from English into Japanese by JST.【JST・京大機械翻訳】

シソーラス用語： *モデル検査 ,  *ネットワーク ,  ビット同期 ,  分散アルゴリズム ,  *保護具 ,  制御装置 ,  パラメタリゼーション ,  位相幾何学
準シソーラス用語： カットオフ ,  論理式 ,  形式的検証 ,  時間付きオートマトン , 【Automatic Indexing@JST】

著者キーワード (4件)： パラメータ化モデル検査 ,  時間付きオートマトン ,  カットオフ定理 ,  パラメータ化システム

分類 (4件)： 図形・画像処理一般  (JE04010I) ,  グラフ理論基礎  (IA02020S) ,  人工知能  (JE08000Z) ,  計算理論  (JB02000A)

タイトルに関連する用語 (4件)： ガード ,  時間付きオートマトン ,  パラメータ化 ,  モデル検査