|
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 KatoenVerifying 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. |
|
| |