文献

J-GLOBAL ID：202202229316471710   整理番号：22A1105020

浮動小数点演算による正しい確率モデル検査【JST・京大機械翻訳】

Correct Probabilistic Model Checking with Floating-Point Arithmetic

著者 (1件)： Hartmanns Arnd (University of Twente, Enschede, The Netherlands)
資料名： Lecture Notes in Computer Science  (Lecture Notes in Computer Science)
巻： 13244  ページ： 41-59  発行年： 2022年 
JST資料番号： H0078D  ISSN： 0302-9743  資料種別： 会議録 (C)
記事区分： 原著論文  発行国： ドイツ (DEU)  言語： 英語 (EN)

抄録/ポイント： 確率的モデル検査は,Markovモデルにおける関心の指定行動に関連する確率と期待値を計算する。形式的検証アプローチとして,それを臨界システムに適用した。したがって,確率的モデルチェッカーが正しい結果をもたらすと確信する。しかし,スケーラビリティと性能を達成するために,これらのツールは,確率と他の値を表現するために有限精度浮動点数を使用する。結果として,それらの結果は,ハードツー予測方法で蓄積し,相互作用するかもしれない丸め誤差により影響される。本論文では,浮動点計算における丸めの方向を制御する現在のハードウェアの能力を利用して,高速で正しい確率的モデル検査を実行する方法を示した。著者らは,高レベルプログラミング言語から正しい丸めを達成する際の合併症を概説し,モデストツールセットmcstaモデルチェッカーの一部として実装を記述し,異なるオペレーティングシステムおよびCPUアーキテクチャにわたる広範な実験評価における性能と正当性の間のトレードオフを例示した。Copyright The Author(s) 2022 Translated from English into Japanese by JST.【JST・京大機械翻訳】

シソーラス用語： 予測技法 ,  相互作用 ,  オペレーティングシステム ,  プログラミング言語 ,  期待値 ,  浮動 ,  臨界 ,  *浮動小数点演算 ,  ハードウェア ,  *確率モデル ,  検証 ,  計算機アーキテクチャ ,  合併症
準シソーラス用語： Markovモデル ,  形式的検証 ,  実験評価 , 【Automatic Indexing@JST】

分類 (2件)： 数値計算  (JE02000J) ,  演算方式  (JC02020Z)

タイトルに関連する用語 (3件)： 浮動小数点演算 ,  確率モデル ,  検査