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  -