Abstraction of Continuous-Time Markov Chains

 

Daniel Willems

Diplomarbeitsvortrag (in English)

 

Continuous-time Markov chains (CTMCs) are a certain type of stochastic
processes. They are being used for performance and dependability
evaluation and can be generated from high-level models such as
stochastic petri-nets and queueing networks. Like in the setting of
transistionsystems, model checking algorithms perform badly on huge
CTMCs and there is the well known state space explosion problem when
generating CTMCs from high-level models. Therefore techniques for
minimising/abstracting CTMCs, which we will take a closer look at, are
of special interest.

In this talk, first a well known abstraction technique for
continuous-time Markov chains based on bisimulation will be presented.
This technique will be extended such that one can merge non-bisimular
states with perferably similar behavior. We will have to introduce the
notation of abstract continuous-time Markov chains (ACTMCs), where
transition rates are no longer deterministic as they are in CTMCs. Then
we will have a look at some abstractions based on probabilistic
simulation instead of bisimulation. We will see that we also need to add
exitrates and transition probabilities to the definition of ACTMCs
(which are implicitly given in CTMCs) to get more precise abstractions.

Since the indeterminism in ACTMCs is similar to the indeterminism in
continuous-time Markov decision processes (CTMDPs), we can adopt the
schedulers from the setting of CTMDPs to handle the indeterminism in
ACTMCs in a formal way. To prevent the schedulers from picking invalid
combinations of rates, exitrates and probabilities in ACTMCs, we will
have to purge the ACTMC from invalid values.

Finally we will note, that model checking for ACTMCs is possible for an
important fragment of CSL. A more detailed view on model checking would
unfortunatly go beyond the scope of this talk.