Verifying Probabilistic Procedural Programs

Javier Esparza, Kousha Etessami

Research output: Chapter in Book/Report/Conference proceedingConference contribution

Abstract

Monolithic finite-state probabilistic programs have been abstractly modeled by finite Markov chains, and the algorithmic verification problems for them have been investigated very extensively. In this paper we survey recent work conducted by the authors together with colleagues on he algorithmic verification of probabilistic procedural programs ([BKS,EKM04,EY04]). Probabilistic procedural programs can more naturally be modeled by recursive Markov chains ([EY04)], or equivalently, probabilistic pushdown automata ([EKM04)]. A very rich theory emerges for these models. While our recent work solves a number of verification problems for these models, many intriguing questions remain open.
Original languageEnglish
Title of host publicationFSTTCS 2004: Foundations of Software Technology and Theoretical Computer Science,
Subtitle of host publication24th International Conference, Chennai, India, December 16-18, 2004, Proceedings
PublisherSpringer Berlin Heidelberg
Pages16-31
Number of pages16
Volume3328
ISBN (Electronic)978-3-540-30538-5
ISBN (Print) 978-3-540-24058-7
DOIs
Publication statusPublished - 2004

Fingerprint

Dive into the research topics of 'Verifying Probabilistic Procedural Programs'. Together they form a unique fingerprint.

Cite this