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.
Preview |
Text
LIPIcs-ICALP-2018-113.pdf - Published Version Download (471kB) | Preview |
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.
| Type: | Proceedings paper |
|---|---|
| Title: | Almost sure productivity |
| Event: | 45th International Colloquium on Automata, Languages, and Programming (ICALP 2018) |
| ISBN-13: | 9783959770767 |
| Open access status: | An open access version is available from UCL Discovery |
| DOI: | 10.4230/LIPIcs.ICALP.2018.113 |
| Language: | English |
| Additional information: | © Alejandro Aguirre, Gilles Barthe, Justin Hsu, and Alexandra Silva; licensed under Creative Commons License CC-BY |
| Keywords: | Coinduction, Probabilistic Programming, Productivity |
| UCL classification: | UCL UCL > Provost and Vice Provost Offices > UCL BEAMS UCL > Provost and Vice Provost Offices > UCL BEAMS > Faculty of Engineering Science UCL > Provost and Vice Provost Offices > UCL BEAMS > Faculty of Engineering Science > Dept of Computer Science |
| URI: | https://discovery.ucl.ac.uk/id/eprint/10056434 |
Archive Staff Only
 |
View Item |
