Institute for Formal Methods in Computer Science
University of Stuttgart
2pm 11 June 2004 (followed by Kousha)
Room 2511, JCMB, King's Buildings
We study probabilistic pushdown systems as a model for probabilistic programs with possibly recursive procedures. We show that, even though the associated Markov chains have an infinite number of states, several model-checking problems are decidable. We mention several open questions.
Joint work with Antonin Kucera and Richard Mayr