TY - GEN TI - Almost sure productivity SP - 113.1 AV - public Y1 - 2018/07/01/ EP - 113.15 N1 - © Alejandro Aguirre, Gilles Barthe, Justin Hsu, and Alexandra Silva; licensed under Creative Commons License CC-BY 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 PB - LIPIcs , Schloss Dagstuhl - Leibniz-Zentrum für Informatik UR - https://discovery.ucl.ac.uk/id/eprint/10056434/ SN - 1868-8969 CY - Prague, Czech Republic A1 - Aguirre, A A1 - Barthe, G A1 - Hsu, J A1 - Silva, A KW - Coinduction KW - Probabilistic Programming KW - Productivity ER -