文献

J-GLOBAL ID：202002271698782870   整理番号：20A2638430

部分可観測性によるプログラミングと推論【JST・京大機械翻訳】

Programming and reasoning with partial observability

著者 (2件)： Atkinson Eric (Massachusetts Institute of Technology, USA) ,  Carbin Michael (Massachusetts Institute of Technology, USA)
資料名： Proceedings of the ACM on Programming Languages  (Proceedings of the ACM on Programming Languages)
巻： 4  号： OOPSLA  ページ： 1-28  発行年： 2020年 
JST資料番号： W5683A  ISSN： 2475-1421  資料種別： 逐次刊行物 (A)
記事区分： 原著論文  発行国： アメリカ合衆国 (USA)  言語： 英語 (EN)

抄録/ポイント： コンピュータプログラムは,部分的に観察可能な環境においてますます展開されている。部分的に観察可能な環境は,その状態がプログラムに完全には見えない環境であるが,プログラムは部分観測を受ける。開発者は,通常,観測を与えられた状態推定器を書き込むことにより,環境の隠れた状態を推論する試みにより,部分可観測性を扱う。安全クリティカルドメインにおいて,安全特性開発者を形式的に検証することは,環境モデルを書き込むかもしれない。モデルは,観測と隠れ状態の間の関係を捕えて,ソフトウェアを修正するために使用する。本論文では,部分的に観察可能な環境におけるプログラムを書き,検証するための新しい方法論を提示した。著者らは,開発者が状態推定を実行するのに自動的に使用する環境モデルを書き込むプログラミング方法論である信念プログラミングを提示する。信念プログラムは,可能な状態を捉える信念状態を動的に更新し,質問する。検証を可能にするために,著者らは,プログラムの可能な状態に関する古典的Hoare論理理由が,信念プログラムの可能な信念状態に関する理由である,Epistemic Hoare Logicを提示する。BLIMPと呼ばれる簡単なコア言語に対する意味論とプログラム論理を定義することにより,これらの概念を開発した。事例研究では,BLIMPにおけるMars Polar Landerの制御装置を書き込み,検証するために,信念プログラミングがどのように使用できるかを示した。CBLIMPと呼ぶBLIMPの実装を提示し,信念プログラミングの実現可能性を決定するためにそれを評価する。Please refer to this article’s citation page on the publisher website for specific rights information. Translated from English into Japanese by JST.【JST・京大機械翻訳】

シソーラス用語： 計算機プログラム ,  意味論 ,  言語 ,  制御装置 ,  不確実性 ,  プログラミング言語 ,  *可観測性 ,  状態推定 ,  ソフトウェア ,  事例研究 ,  環境モデル
準シソーラス用語： Hoare論理 , 【Automatic Indexing@JST】

著者キーワード (4件)： 論理 ,  部分可観測性 ,  プログラミング言語 ,  不確実性

分類 (2件)： 人工知能  (JE08000Z) ,  計算理論  (JB02000A)

タイトルに関連する用語 (3件)： 可観測性 ,  プログラミング ,  推論