Model Checking Recursive Probabilistic Programs with Conditioning
arxiv(2024)
摘要
We address the problem of model checking temporal logic specifications for
probabilistic programs with recursive procedures, nested queries, and
conditioning expressed with observe statements. We introduce probabilistic
Operator Precedence Automata (pOPA), a new class of probabilistic pushdown
automata suitable to model constructs and behaviors of probabilistic programs.
We develop a model checking algorithm that can verify requirements expressed in
a fragment of Precedence Oriented Temporal Logic (POTL^f_𝒳) on a
pOPA in single EXPTIME. POTL^f_𝒳 is a temporal logic based on
Operator Precedence Languages, which features modalities that interact with the
context-free structure of program traces, matching procedure calls with returns
or observe statements. We provide the first probabilistic model checking
implementation of context-free language properties for probabilistic pushdown
systems.
更多查看译文
AI 理解论文
溯源树
样例
生成溯源树,研究论文发展脉络
Chat Paper
正在生成论文摘要