Interactive version: .

Continuous-time Markov chains (CTMCs)

Background

In this section, we explain how Stormpy can be used to build a simple CTMC. Building CTMCs works similar to building DTMCs as in Discrete-time Markov chains (DTMCs), however instead of transition probabilities we use transition rates.

01-building-ctmcs.py

First, we import Stormpy:

>>> import stormpy

Transition Matrix

In this example, we build the transition matrix using a numpy array

>>> import numpy as np
>>> transitions = np.array([
...    [0, 1.5, 0, 0],
...    [3, 0, 1.5, 0],
...    [0, 3, 0, 1.5],
...    [0, 0, 3, 0], ], dtype='float64')

The following function call returns a sparse matrix with default row groups:

>>> transition_matrix = stormpy.build_sparse_matrix(transitions)
>>> print(transition_matrix)

                0       1       2       3
        ---- group 0/3 ----
0       (       0       1.5     0       0               )       0
        ---- group 1/3 ----
1       (       3       0       1.5     0               )       1
        ---- group 2/3 ----
2       (       0       3       0       1.5             )       2
        ---- group 3/3 ----
3       (       0       0       3       0               )       3
                0       1       2       3

Labeling

The state labeling is created analogously to the previous example in building DTMCs:

>>> state_labeling = stormpy.storage.StateLabeling(4)
>>> state_labels = {'empty', 'init', 'deadlock', 'full'}
>>> for label in state_labels:
...    state_labeling.add_label(label)
>>> state_labeling.add_label_to_state('init', 0)
>>> state_labeling.add_label_to_state('empty', 0)
>>> state_labeling.add_label_to_state('full', 3)

Building the Model

Now, we can collect all components, including the choice labeling. To let the transition values be interpreted as rates we set rate_transitions to True:

>>> components = stormpy.SparseModelComponents(transition_matrix=transition_matrix, state_labeling=state_labeling, rate_transitions=True)

And finally, we can build the model:

>>> ctmc = stormpy.storage.SparseCtmc(components)
>>> print(ctmc)

--------------------------------------------------------------
Model type:     CTMC (sparse)
States:         4
Transitions:    6
Reward Models:  none
State Labels:   4 labels
   * init -> 1 item(s)
   * full -> 1 item(s)
   * empty -> 1 item(s)
   * deadlock -> 0 item(s)
Choice Labels:  none
--------------------------------------------------------------