Campus Event Calendar
Event Entry
What and Who
A nugget of probable truth
Prof. Javier Esparza
Uni Stuttgart
Talk
AG 1, AG 2, AG 3, AG 4, AG 5
MPI Audience
Note: We use this to send email in the morning.
Date, Time and Location
Wednesday, 25 January 2006
16:00
-- Not specified --
46.1 - MPII
R 024
Saarbrücken
Abstract
Imperative programming languages provide procedural mechanisms for
structuring large programs. In the last years our group has used pushdown
automata to model and verify programs with (possibly recursive)
procedures.
Currently, we (and other groups using our tools) are able to check
relevant
properties of programs with up to ten thousands of lines within few
minutes.
A fascinating current challenge is the verification of probabilistic
programs. Stochastic decisions can be an intrinsic part of the program,
as in randomized algorithms, or can be added to it in order to
model our limited knowledge of the program or of its environment.
While finite Markov chains provide a resonable
semantics for probabilistic while programs, probabilistic pushdown
automata (or
equivalent models like recursive Markov chains) must be used in the
procedural case. These models generate infinite Markov chains, and so
many of the basic results of Markov chain theory, which are only valid
for finite chains, cannot be applied.
In the talk I will first summarize our work on the non-probabilistic
case. I will then proceed to present algorithms and complexity bounds
for some representative problems on verification
of probabilistic pushdown automata. They concern
the probability of termination, the expected running time, and the
expected time it takes to serve a request.
The talk is based on joint work with Tomasz Brazdil, Tony Kucera, and
Richard Mayr, but also on the work of our friendly competitors,
Kousha Etessami and Mihalis Yannakakis.
Here is a quiz question for you, probably not difficult to answer with
Google at your
fingertips: Guess the reason for the talk's title. Hint: it has to
do with the talk's date.
structuring large programs. In the last years our group has used pushdown
automata to model and verify programs with (possibly recursive)
procedures.
Currently, we (and other groups using our tools) are able to check
relevant
properties of programs with up to ten thousands of lines within few
minutes.
A fascinating current challenge is the verification of probabilistic
programs. Stochastic decisions can be an intrinsic part of the program,
as in randomized algorithms, or can be added to it in order to
model our limited knowledge of the program or of its environment.
While finite Markov chains provide a resonable
semantics for probabilistic while programs, probabilistic pushdown
automata (or
equivalent models like recursive Markov chains) must be used in the
procedural case. These models generate infinite Markov chains, and so
many of the basic results of Markov chain theory, which are only valid
for finite chains, cannot be applied.
In the talk I will first summarize our work on the non-probabilistic
case. I will then proceed to present algorithms and complexity bounds
for some representative problems on verification
of probabilistic pushdown automata. They concern
the probability of termination, the expected running time, and the
expected time it takes to serve a request.
The talk is based on joint work with Tomasz Brazdil, Tony Kucera, and
Richard Mayr, but also on the work of our friendly competitors,
Kousha Etessami and Mihalis Yannakakis.
Here is a quiz question for you, probably not difficult to answer with
Google at your
fingertips: Guess the reason for the talk's title. Hint: it has to
do with the talk's date.
Contact
Roxane Wetzel
9325-900
--email hidden
passcode not visible
logged in users only
Roxane Wetzel, 01/16/2006 15:37
Roxane Wetzel, 01/16/2006 15:36 -- Created document.
Roxane Wetzel, 01/16/2006 15:36 -- Created document.