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:

[1]:

>>> import stormpy


## Transition Matrix¶

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

[2]:

>>> 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:

[3]:

>>> 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:

[4]:

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


## 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:

[5]:

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


And finally, we can build the model:

[6]:

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

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