文献

J-GLOBAL ID：202202227196941513   整理番号：22A1053070

再帰的確率プログラムの時間特性のモデル検査【JST・京大機械翻訳】

Model Checking Temporal Properties of Recursive Probabilistic Programs

著者 (3件)： Winkler Tobias (RWTH Aachen University, Aachen, Germany) ,  Gehnen Christina (RWTH Aachen University, Aachen, Germany) ,  Katoen Joost-Pieter (RWTH Aachen University, Aachen, Germany)
資料名： Lecture Notes in Computer Science  (Lecture Notes in Computer Science)
巻： 13242  ページ： 449-469  発行年： 2022年 
JST資料番号： H0078D  ISSN： 0302-9743  資料種別： 会議録 (C)
記事区分： 原著論文  発行国： ドイツ (DEU)  言語： 英語 (EN)

抄録/ポイント： 確率的プッシュダウンオートマトン(pPDA)は,離散ランダム選択,手順,およびリターンを含むプログラミング言語のための標準操作モデルである。時間的特性は,プログラム実行中のイベントの年代順への洞察を得るために有用である。文献における既存のアプローチは,主に[数式:原文を参照]規則およびLTL特性に集中している。本論文では,CaRetのような仕様論理により記述でき,[数式:原文を参照]正規特性よりも厳密に表現できる[数式:原文を参照]可視プッシュダウン言語に対するpPDAのモデル検査問題を研究した。これらの論理式により,手続きプログラムから生じる構造化計算を明示的に取り入れる特性を特定することが可能である。例えば,CaRetは,対応する将来のリターンと対応できる手順を一致させ,従って,全体および部分の正当性のような基本的なプログラム特性を表現することができる。Copyright The Author(s) 2022 Translated from English into Japanese by JST.【JST・京大機械翻訳】

シソーラス用語： 言語 ,  プログラミング言語 ,  プッシュダウンオートマトン ,  計算 ,  イベント ,  プログラム実行 ,  無作為抽出 ,  *モデル検査
準シソーラス用語： 論理式 , 【Automatic Indexing@JST】

著者キーワード (5件)： 確率的再帰プログラム ,  モデル検査 ,  確率的プッシュダウンオートマトン ,  視覚的プッシュダウン言語 ,  CaRet

分類 (2件)： オートマトン理論  (JB04000O) ,  計算機システム開発  (JD02010R)

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