Campus Event Calendar
Event Entry
What and Who
PhD Application Talk: PASS: Predicate Abstraction in Probabilistic Model Checking
Ernst Moritz Hahn
Talk
AG 1, AG 2, AG 3, AG 4, AG 5, SWS, RG1, RG2
MPI Audience
English
Note: We use this to send email in the morning.
Date, Time and Location
Monday, 25 February 2008
09:00
330 Minutes
E1 4
024
Saarbrücken
Abstract
Probabilistic Model Checking has had successful applications in
various areas, including the verification of embedded protocol
software, real-time systems and even biological systems. However,
many interesting models have a statespace which is too large to fit
in memory of todays computers or are even infinite. Predicate
abstraction is a technique with which many nondeterministic models
containing infinite statespace where successfully handled. There has
also been research on predicate abstraction for probabilistic
systems. Former results had the restriction that for predicate
abstraction to be used, the whole statespace of the models had to be
generated, which made this technique was still infeasible in many
cases. In the talk I am going to hold, I introduce PASS, which is a
software tool allowing to do predicate abstraction of systems
containing probabilities without the need of generating the
statespace of the original model beforehand.
various areas, including the verification of embedded protocol
software, real-time systems and even biological systems. However,
many interesting models have a statespace which is too large to fit
in memory of todays computers or are even infinite. Predicate
abstraction is a technique with which many nondeterministic models
containing infinite statespace where successfully handled. There has
also been research on predicate abstraction for probabilistic
systems. Former results had the restriction that for predicate
abstraction to be used, the whole statespace of the models had to be
generated, which made this technique was still infeasible in many
cases. In the talk I am going to hold, I introduce PASS, which is a
software tool allowing to do predicate abstraction of systems
containing probabilities without the need of generating the
statespace of the original model beforehand.
Contact
IMPRS-CS
225
--email hidden
passcode not visible
logged in users only
Tags, Category, Keywords and additional notes
Please note: The talks will take place in random order!
Lourdes Lara-Tapia, 02/21/2008 17:32 -- Created document.