Lyngby, Denmark, 14-16 October 2009
NWPT '09 Home|
Call for papers
Joost Pieter Katoen
Verifying Large --and Infinite-- Markov ChainsModel 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.