Lower Bounds for Possibly Divergent Probabilistic Programs

Autor:	Shenghua Feng, Mingshuai Chen, Han Su, Benjamin Lucien Kaminski, Joost-Pieter Katoen, Naijun Zhan
Rok vydání:	2023
Předmět:	FOS: Computer and information sciences Computer Science - Logic in Computer Science Probability (math.PR) FOS: Mathematics ddc:004 Safety Risk Reliability and Quality Mathematics - Probability Software Logic in Computer Science (cs.LO)
Zdroj:	Proceedings of the ACM on programming languages 7(OOPSLA1), 99 (2023). doi:10.1145/3586051 International Conference on Object-Oriented Programming Systems, Languages, and Applications, OOPSLA 2023, Cascais, Portugal, 2023-10-23-2023-10-27
DOI:	10.48550/arxiv.2302.06082
Popis:	We present a new proof rule for verifying lower bounds on quantities of probabilistic programs. Our proof rule is not confined to almost-surely terminating programs -- as is the case for existing rules -- and can be used to establish non-trivial lower bounds on, e.g., termination probabilities and expected values, for possibly divergent probabilistic loops, e.g., the well-known three-dimensional random walk on a lattice. Comment: Paper conditionally accepted by OOPSLA 2023
Databáze:	OpenAIRE
Externí odkaz:	https://explore.openaire.eu/search/publication?articleId=doi_dedup___::1e7f77b1c130d22c5d52946d36d60087 Zobrazit plný text záznamu