21st Nordic Workshop on Programming Theory, NWPT '09
Lyngby, Denmark, 14-16 October 2009
NWPT '09 Home
Call for papers
Organisation
Important Dates

Programme

Background
Scope
Invited Talks
Submission
Publication
Venue
Registration
Accommodation
Travel info

Joost Pieter Katoen

Verifying Large --and Infinite-- Markov Chains

Model checking of probabilistic models is used in many different areas such as performance and dependability evaluation, security protocols, randomized algorithms, and biological systems. Tools have been successfully applied to numerous case studies, but like in traditional model checking, the state explosion problem forms a serious limitation. Although many techniques from traditional model checking have been generalized towards probabilistic models such as BDDs and partial-order reduction, more aggressive reduction techniques are needed. In this talk, we introduce model checking of continuous-time Markov chains (CTMCs), present a three-valued abstraction technique, and present several examples to show its effectiveness when applied to huge, and even infinite CTMCs such as arising from systems biology and classical performance analysis, i.e., queuing networks.
http://www.imm.dtu.dk/nwpt09 | email: nwpt09(at)imm.dtu.dk | © DTU Informatics, 2009