@inproceedings{discovery10056434,
           pages = {113.1--113.15},
       booktitle = {Proceedings of the 45th International Colloquium on Automata, Languages, and Programming (ICALP 2018)},
          volume = {107},
         address = {Prague, Czech Republic},
            note = {{\copyright} Alejandro Aguirre, Gilles Barthe, Justin Hsu, and Alexandra Silva; licensed under Creative Commons License CC-BY},
       publisher = {LIPIcs , Schloss Dagstuhl - Leibniz-Zentrum f{\"u}r Informatik},
            year = {2018},
           title = {Almost sure productivity},
         journal = {Leibniz International Proceedings in Informatics, LIPIcs},
           month = {July},
        keywords = {Coinduction, Probabilistic Programming, Productivity},
             url = {https://discovery.ucl.ac.uk/id/eprint/10056434/},
            issn = {1868-8969},
          author = {Aguirre, A and Barthe, G and Hsu, J and Silva, A},
        abstract = {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{\"o}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.}
}