"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."@en . "978-3-642-22109-5" . "10.1007/978-3-642-22110-1" . . "Snowbird, UT, USA" . . . . "Efficient Analysis of Probabilistic Programs with an Unbounded Counter" . "Springer-Verlag" . "3"^^ . "RIV/00216224:14330/11:00054480" . . . . "Computer Aided Verification, 23rd International Conference, CAV 2011" . "14330" . "Efficient Analysis of Probabilistic Programs with an Unbounded Counter"@en . . "2"^^ . . . "17"^^ . "P(1M0545)" . "[467A6D34EA24]" . . "Efficient Analysis of Probabilistic Programs with an Unbounded Counter" . "RIV/00216224:14330/11:00054480!RIV12-MSM-14330___" . . "196741" . "Kiefer, Stefan" . "Ku\u010Dera, Anton\u00EDn" . . . "Efficient Analysis of Probabilistic Programs with an Unbounded Counter"@en . . "one-counter machines; probabilistic systems; model-checking"@en . "2011-07-14+02:00"^^ . . . "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." . "Berlin" . . "Br\u00E1zdil, Tom\u00E1\u0161" .