eprintid: 10056434 rev_number: 19 eprint_status: archive userid: 608 dir: disk0/10/05/64/34 datestamp: 2018-09-27 10:57:09 lastmod: 2021-09-18 21:46:36 status_changed: 2018-09-27 10:57:09 type: proceedings_section metadata_visibility: show creators_name: Aguirre, A creators_name: Barthe, G creators_name: Hsu, J creators_name: Silva, A title: Almost sure productivity ispublished: pub divisions: UCL divisions: B04 divisions: C05 divisions: F48 keywords: Coinduction, Probabilistic Programming, Productivity note: © Alejandro Aguirre, Gilles Barthe, Justin Hsu, and Alexandra Silva; licensed under Creative Commons License CC-BY 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ö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. date: 2018-07-01 date_type: published publisher: LIPIcs , Schloss Dagstuhl - Leibniz-Zentrum für Informatik oa_status: green full_text_type: pub language: eng primo: open primo_central: open_green verified: verified_manual elements_id: 1584194 doi: 10.4230/LIPIcs.ICALP.2018.113 isbn_13: 9783959770767 lyricists_name: Silva, Alexandra lyricists_id: ASILV10 actors_name: Bracey, Alan actors_id: ABBRA90 actors_role: owner full_text_status: public publication: Leibniz International Proceedings in Informatics, LIPIcs volume: 107 place_of_pub: Prague, Czech Republic pagerange: 113.1-113.15 event_title: 45th International Colloquium on Automata, Languages, and Programming (ICALP 2018) issn: 1868-8969 book_title: Proceedings of the 45th International Colloquium on Automata, Languages, and Programming (ICALP 2018) citation: Aguirre, A; Barthe, G; Hsu, J; Silva, A; (2018) Almost sure productivity. In: Proceedings of the 45th International Colloquium on Automata, Languages, and Programming (ICALP 2018). (pp. 113.1-113.15). LIPIcs , Schloss Dagstuhl - Leibniz-Zentrum für Informatik: Prague, Czech Republic. Green open access document_url: https://discovery.ucl.ac.uk/id/eprint/10056434/1/LIPIcs-ICALP-2018-113.pdf