Efficient Analysis of Probabilistic Programs with an Unbounded Counter
- Submitting institution
-
University of Oxford
- Unit of assessment
- 11 - Computer Science and Informatics
- Output identifier
- 2089
- Type
- D - Journal article
- DOI
-
10.1145/2629599
- Title of journal
- Journal of the ACM
- Article number
- -
- First page
- 1
- Volume
- 61
- Issue
- 6
- ISSN
- 0004-5411
- Open access status
- Out of scope for open access requirements
- Month of publication
- December
- Year of publication
- 2014
- URL
-
-
- Supplementary information
-
-
- Request cross-referral to
- -
- Output has been delayed by COVID-19
- No
- COVID-19 affected output statement
- -
- Forensic science
- No
- Criminology
- No
- Interdisciplinary
- No
- Number of additional authors
-
2
- Research group(s)
-
-
- Citation count
- 7
- Proposed double-weighted
- No
- Reserve for an output with double weighting
- No
- Additional information
- One-counter automata model programs with unbounded variables have an infinite state space. In the probabilistic case, analysing such programs requires the computation of quantities such as the expectation and distribution of the termination time, and the probability of satisfying omega-regular specifications. Based on martingale techniques, this paper provides efficient algorithms for the quantitative analysis of probabilistic programs. The techniques introduced here have been taken up by, for example, Br�zdil et al. in ATVA�16 (https://doi.org/10.1007/978-3-319-46520-3_3) and Mayr et al. in LICS�17 (10.1109/LICS.2017.8005131).
- Author contribution statement
- -
- Non-English
- No
- English abstract
- -
