多項式確率プログラムの自動停止解析【JST・京大機械翻訳】

抄録/ポイント：

抄録/ポイント
文献の概要を数百字程度の日本語でまとめたものです。
部分表示の続きは、JDreamⅢ(有料)でご覧頂けます。
J-GLOBALでは書誌(タイトル、著者名等)登載から半年以上経過後に表示されますが、医療系文献の場合はMyJ-GLOBALでのログインが必要です。

確率的プログラムの終端挙動はランダム割当ての結果に依存する。ほとんど確実な終了(AST)は,プログラムがすべての可能な入力で確率で終わるかどうかという疑問に関係する。正のほぼ確実な終端(PAST)は,有限予想数のステップにおける終端に焦点を合わせる。本論文では,そのガードと表現が多項式表現である確率的プログラムの終端解析に対する完全自動化手法を提案した。証明(陽性)ASTは,一般的には不可能であり,既存の証明規則は,通常,十分条件を提供する。これらの条件は,主に,超境界の制約を含む。文献からの4つの証明規則を考察し,(P)ASTに対する既存の証明規則の一般化でこれらを拡張した。プログラム変数上の多項式に関する漸近的限界を効果的に計算することによって,得られた証明規則のセットを自動化した。これらの限界を用いて,証明ルールの超境界の制約を含む十分条件を決定した。したがって,ソフトウェアツールAmberは,多項式確率プログラムの大規模クラスのためのそれらの否定と同様にAST,PASTをチェックでき,一方,多項式 w度で終了推論を完全に実行した。実験結果は,著者らの一般化証明規則の利点を示し,Amberが,他の最先端のツールのための到達から外れる確率的プログラムを扱うことができることを示した。【JST・京大機械翻訳】