Almost Sure Productivity
Alejandro Aguirre, Gilles Barthe, Justin Hsu, Alexandra Silva

TL;DR
The paper introduces Almost Sure Productivity (ASP), a probabilistic extension of productivity for coinductive structures, with methods to verify ASP using syntactic criteria and model-checking, proving its decidability.
Contribution
It formalizes ASP for probabilistic streams and trees, and provides verification techniques including a syntactic criterion and a reduction to model-checking, establishing decidability.
Findings
ASP is defined using coalgebra semantics.
A core language for probabilistic streams and trees is introduced.
ASP verification is decidable via reduction to pCTL* model-checking.
Abstract
We define Almost Sure Productivity (ASP), a probabilistic generalization of the productivity condition for coinductively defined structures. Intuitively, a probabilistic coinductive stream or tree is ASP if it produces infinitely many outputs with probability 1. Formally, we define almost sure productivity using a final coalgebra semantics of programs inspired from Kerstan and K\"onig. Then, we introduce a core language for probabilistic streams and trees, and provide two approaches to verify ASP: a sufficient syntactic criterion, and a reduction to model-checking pCTL* formulas on probabilistic pushdown automata. The reduction shows that ASP is decidable for our core language.
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.
