文献

J-GLOBAL ID：201802288491338676   整理番号：18A1130852

確率論理CSL-TAの効率的モデル検査【JST・京大機械翻訳】

Efficient model checking of the stochastic logic CSL^TA

著者 (2件)： Amparore E.G. (Dipartimento di Informatica, Universita di Torino, Italy) ,  Donatelli S. (Dipartimento di Informatica, Universita di Torino, Italy)
資料名： Performance Evaluation  (Performance Evaluation)
巻： 123-124  ページ： 1-34  発行年： 2018年 
JST資料番号： C0647B  ISSN： 0166-5316  CODEN： PEEVD9  資料種別： 逐次刊行物 (A)
記事区分： 原著論文  発行国： オランダ (NLD)  言語： 英語 (EN)

抄録/ポイント： CSL-TAは,良く知られたCSLを含む連続時間Markov連鎖(CTMCs)の確率的時間論理である。CSL-TA特性は,単一クロック決定的タイミングオートマトン(DTAs)を用いて定義される。最悪ケースにおけるCSL~TA量のモデル検査は,|CTMC|×|DTA|のサイズの非エルゴード的Markov再生プロセス(MRGP)の定常状態確率の計算に対するものである。種々のMRGP解法は文献で利用可能であり,MRGPにおいて,ある成分は実際により低いコスト(CTMC解と同じコスト)で解かれることを認識することにより,非エルゴードMRGPの定常状態分布を計算する。残念ながら,この技術は依然としてMRGP全体の構築を必要とする。本論文は,様々なCSL-TAモデル検査アルゴリズムを考案するために,成分方法を適用して,前方および後方であった。この要素法は,CTMCとDTAから構築されたMRGPに適用できる。この方法は,CTMCから構築されたMRGPとDTAの領域グラフ,DTAの時間到達可能性を考慮した構築,および多くの場合,考慮されたMRGP状態の著しい減少を可能にする。両方の場合において,MRGP全体を構築した。本論文の主要な結果は,成分同定がDTAの領域グラフだけに基づいているモデル検査アルゴリズムを考案する代わりにある。MRGP構成要素は,領域グラフの構成要素から出発して,必要とされるとき,「オンザフライ」として生成される。次に,それらを最も安価な利用可能な解法で解いた。一度成分が解決されると,全MRGPは構築されず,解決されない。オンザフライアルゴリズムは「適応型」である:時間と空間は公式に依存し,DTAがCSL特性を実際に表現するとき,アルゴリズムの複雑さは標準CSLモデル検査アルゴリズムのそれにシームレスに減少する。Copyright 2018 Elsevier B.V., Amsterdam. All rights reserved. Translated from English into Japanese by JST.【JST・京大機械翻訳】

シソーラス用語： グラフ ,  確率モデル ,  CASE ,  クロック ,  時間論理 ,  連続時間系 ,  *モデル検査 ,  アルゴリズム ,  Markov連鎖
準シソーラス用語： シームレス ,  アルゴリズム複雑性 ,  低価格 ,  定常状態 ,  *確率論理 , 【Automatic Indexing@JST】

著者キーワード (5件)： 確率モデル検査 ,  CSL-TA ,  Markov再生プロセス(MRGP) ,  経路特性 ,  時間付きオートマトン

分類 (2件)： 計算理論  (JB02000A) ,  計算機システム開発  (JD02010R)

タイトルに関連する用語 (3件)： 確率論理 ,  Ta ,  モデル検査