Model Checking Recursive Probabilistic Programs with Conditioning
<|reference_start|>Model Checking Recursive Probabilistic Programs with Conditioning: 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_\mathcal{X}$) on a pOPA in single EXPTIME. POTL$^f_\mathcal{X}$ 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.<|reference_end|>
@article{pontiggia2024model,
    title={Model Checking Recursive Probabilistic Programs with Conditioning},
    author={Francesco Pontiggia, Ezio Bartocci and Michele Chiari},
    journal={arXiv preprint arXiv:2404.03515},
    year={2024},
    archivePrefix={arXiv},
    eprint={2404.03515},
    primaryClass={cs.LO cs.PL}
}