Copenhagen Programming Language Seminar

Time-Bounded Model Checking of Infinite-State Continuous-Time Markov Chains

Dr Lijun Zhang
Saarland University

Wednesday, August 5, 2009, 13:00-14:00
The IT University, Rued Langgaards Vej 7, DK-2300, Auditorium 2


Continuous-time Markov chains (CTMCs) are popular in performance and dependability analysis, and also in biological modeling. In the context of CTMCs, properties of interest can be specified using continuous stochastic logic (CSL), which is a branching-time temporal logic inspired by CTL. We consider the model checking problem over infinite CTMCs, and focus on time-bounded probabilistic properties, expressible in a subset of CSL. This comprises important dependability measures, such as time-bounded probabilistic reachability, and various availability measures like instantaneous, conditional instantaneous and interval availabilities. Conventional model checkers explore the given model exhaustively, which is often costly, due to state explosion, and sometimes impossible because the model is infinite. This talk discusses a method that only explores the model up to a finite depth. The required depth is determined on the fly by an algorithm that is configurable in order to adapt to the characteristics of different classes of models.

Scientific host:Jens Chr. Godskesen Administrative host: Annette Enggaard. All are welcome.
The Copenhagen Programming Language Seminar (COPLAS) is a collaboration between DIKU, ITU, KVL and RUC.
COPLAS is sponsored by the FIRST Graduate School.
To receive information about COPLAS talks by email, send a message to prog-lang-request@mail.it-c.dk with the word 'subscribe' as subject or in the body.

For more information about COPLAS, see http://www.coplas.org