TY - GEN N1 - © Alejandro Aguirre, Gilles Barthe, Justin Hsu, and Alexandra Silva; licensed under Creative Commons License CC-BY TI - Almost sure productivity AV - public Y1 - 2018/07/01/ SP - 113.1 EP - 113.15 CY - Prague, Czech Republic A1 - Aguirre, A A1 - Barthe, G A1 - Hsu, J A1 - Silva, A KW - Coinduction KW - Probabilistic Programming KW - Productivity N2 - We introduce 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 ASP using a final coalgebra semantics of programs inspired by Kerstan and König. Then, we introduce a core language for probabilistic streams and trees, and provide two approaches to verify ASP: a syntactic sufficient criterion, and a decision procedure by reduction to model-checking LTL formulas on probabilistic pushdown automata. ID - discovery10056434 UR - https://discovery.ucl.ac.uk/id/eprint/10056434/ PB - LIPIcs , Schloss Dagstuhl - Leibniz-Zentrum für Informatik SN - 1868-8969 ER -