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)
   * empty -> 1 item(s)
   * deadlock -> 0 item(s)
   * full -> 1 item(s)
Choice Labels:  none
--------------------------------------------------------------