---
res:
bibo_abstract:
- 'In this paper, we consider termination of probabilistic programs with real-valued
variables. The questions concerned are: (a) qualitative ones that ask (i) whether
the program terminates with probability 1 (almost-sure termination) and (ii) whether
the expected termination time is finite (finite termination); (b) quantitative
ones that ask (i) to approximate the expected termination time (expectation problem)
and (ii) to compute a bound B such that the probability to terminate after B steps
decreases exponentially (concentration problem). To solve these questions, we
utilize the notion of ranking supermartingales which is a powerful approach for
proving termination of probabilistic programs. In detail, we focus on algorithmic
synthesis of linear ranking-supermartingales over affine probabilistic programs
(APP''s) with both angelic and demonic non-determinism. An important subclass
of APP''s is LRAPP which is defined as the class of all APP''s over which a linear
ranking-supermartingale exists. Our main contributions are as follows. Firstly,
we show that the membership problem of LRAPP (i) can be decided in polynomial
time for APP''s with at most demonic non-determinism, and (ii) is NP-hard and
in PSPACE for APP''s with angelic non-determinism; moreover, the NP-hardness result
holds already for APP''s without probability and demonic non-determinism. Secondly,
we show that the concentration problem over LRAPP can be solved in the same complexity
as for the membership problem of LRAPP. Finally, we show that the expectation
problem over LRAPP can be solved in 2EXPTIME and is PSPACE-hard even for APP''s
without probability and non-determinism (i.e., deterministic programs). Our experimental
results demonstrate the effectiveness of our approach to answer the qualitative
and quantitative questions over APP''s with at most demonic non-determinism.@eng'
bibo_authorlist:
- foaf_Person:
foaf_givenName: Krishnendu
foaf_name: Chatterjee, Krishnendu
foaf_surname: Chatterjee
foaf_workInfoHomepage: http://www.librecat.org/personId=2E5DCA20-F248-11E8-B48F-1D18A9856A87
orcid: 0000-0002-4561-241X
- foaf_Person:
foaf_givenName: Hongfei
foaf_name: Fu, Hongfei
foaf_surname: Fu
foaf_workInfoHomepage: http://www.librecat.org/personId=3AAD03D6-F248-11E8-B48F-1D18A9856A87
- foaf_Person:
foaf_givenName: Petr
foaf_name: Novotny, Petr
foaf_surname: Novotny
foaf_workInfoHomepage: http://www.librecat.org/personId=3CC3B868-F248-11E8-B48F-1D18A9856A87
- foaf_Person:
foaf_givenName: Rouzbeh
foaf_name: Hasheminezhad, Rouzbeh
foaf_surname: Hasheminezhad
bibo_doi: 10.1145/2837614.2837639
bibo_volume: 20-22
dct_date: 2016^xs_gYear
dct_language: eng
dct_publisher: ACM@
dct_title: Algorithmic analysis of qualitative and quantitative termination problems
for affine probabilistic programs@
...