Efficient Analysis of Probabilistic Programs with an Unbounded Counter
| Authors | |
|---|---|
| Year of publication | 2011 |
| Type | Article in Proceedings |
| Conference | Computer Aided Verification, 23rd International Conference, CAV 2011 |
| MU Faculty or unit | |
| Citation | |
| Doi | http://dx.doi.org/10.1007/978-3-642-22110-1 |
| Field | Informatics |
| Keywords | one-counter machines; probabilistic systems; model-checking |
| Description | We show that a subclass of infinite-state probabilistic programs that can be modeled by probabilistic one-counter automata (pOC) admits an efficient quantitative analysis. In particular, we show that the expected termination time can be approximated up to an arbitrarily small relative error with polynomially many arithmetic operations, and the same holds for the probability of all runs that satisfy a given omega-regular property. |
| Related projects: |