--- res: bibo_abstract: - 'In this article, we consider the termination problem of probabilistic programs with real-valued variables. Thequestions concerned are: 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); andquantitative ones that ask (i) to approximate the expected termination time (expectation problem) and (ii) tocompute a boundBsuch that the probability not to terminate afterBsteps decreases exponentially (con-centration problem). To solve these questions, we utilize the notion of ranking supermartingales, which isa powerful approach for proving termination of probabilistic programs. In detail, we focus on algorithmicsynthesis of linear ranking-supermartingales over affine probabilistic programs (Apps) with both angelic anddemonic non-determinism. An important subclass of Apps is LRApp which is defined as the class of all Appsover which a linear ranking-supermartingale exists.Our main contributions are as follows. Firstly, we show that the membership problem of LRApp (i) canbe decided in polynomial time for Apps with at most demonic non-determinism, and (ii) isNP-hard and inPSPACEfor Apps with angelic non-determinism. Moreover, theNP-hardness result holds already for Appswithout probability and demonic non-determinism. Secondly, we show that the concentration problem overLRApp can be solved in the same complexity as for the membership problem of LRApp. Finally, we show thatthe expectation problem over LRApp can be solved in2EXPTIMEand isPSPACE-hard even for Apps withoutprobability and non-determinism (i.e., deterministic programs). Our experimental results demonstrate theeffectiveness of our approach to answer the qualitative and quantitative questions over Apps with at mostdemonic 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: Novotný, Petr foaf_surname: Novotný 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/3174800 bibo_issue: '2' bibo_volume: 40 dct_date: 2018^xs_gYear dct_identifier: - UT:000434634500003 dct_isPartOf: - http://id.crossref.org/issn/0164-0925 dct_language: eng dct_publisher: Association for Computing Machinery (ACM)@ dct_title: Algorithmic analysis of qualitative and quantitative termination problems for affine probabilistic programs@ ...