Aguirre, Alejandro
[Author];
Barthe, Gilles
[Author];
Hsu, Justin
[Author];
Silva, Alexandra
[Author]
;
Alejandro Aguirre and Gilles Barthe and Justin Hsu and Alexandra Silva
[Contributor]
Footnote:
Diese Datenquelle enthält auch Bestandsnachweise, die nicht zu einem Volltext führen.
Description:
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.