[Club2] talk by Johannes Hölzl: Thursday, Dec. 5, 10:00, Room: John v. Neumann (00.11.038)

[Andrei Popescu]

Dear All,  

This Thursday, Johannes will talk about his work on formalizing 
probabilistic model checking.   

Please note the unusual time and place of the talk.  

Cheers, 
  Andrei  


Probabilistic Models in Interactive Theorem Provers
Johannes Hölzl
======================================================================
Thursday, Dec. 5, 10:00, Room: John v. Neumann (00.11.038) 

Johannes Hölzl works on formalizing probabilistic models in the
interactive theorem prover Isabelle/HOL. For this a formalization of
Markov chain theory and Markov decision process theory is necessary.

To guide and validate the development of these theories probabilistic
model checking is verified. The MC formalization was already used to
proof soundness and completeness of PCTL model checking on rewarded MCs.
Also properties of two distributed protocols where verified: the
ZeroConf protocol and the Crowds anonymity service.

His current work is to formalize MDP theory. He will present an
algorithm to verify results of reachability problems on MDPs in
Isabelle/HOL. This is a central part to use results of probabilistic
model checkers in Isabelle/HOL. The developed theories are central part
for verifying PCTL model checking on MDPs.

This talk tries to present interactive theorem proving from a
model checking perspective. And, to give an overview what is already
possible in ITPs with regard to probabilistic models.
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <https://mailmanbroy.informatik.tu-muenchen.de/pipermail/club2/attachments/20131203/3b844ea8/attachment.html>