Interactive version: .

# Markov automata (MAs)¶

## Background¶

We already saw the process of building CTMCs and MDPs via Stormpy.

Markov automata use states that are probabilistic, i.e. like the states of an MDP, or Markovian, i.e. like the states of a CTMC.

In this section, we build a small MA with five states from which the first four are Markovian. Since we covered labeling and exit rates already in the previous examples we omit the description of these components. The full example can be found here:

01-building-mas.py

First, we import Stormpy:

[1]:

>>> import stormpy


## Transition Matrix¶

For building MDPS, we used the SparseMatrixBuilder to create a matrix with a custom row grouping. In this example, we use the numpy library.

In the beginning, we create a numpy array that will be used to build the transition matrix of our model.:

[2]:

>>> import numpy as np
>>> transitions = np.array([
...        [0, 1, 0, 0, 0],
...        [0.8, 0, 0.2, 0, 0],
...        [0.9, 0, 0, 0.1, 0],
...        [0, 0, 0, 0, 1],
...        [0, 0, 0, 1, 0],
...        [0, 0, 0, 0, 1]], dtype='float64')


When building the matrix we define a custom row grouping by passing a list containing the starting row of each row group in ascending order:

[3]:

>>> transition_matrix = stormpy.build_sparse_matrix(transitions, [0, 2, 3, 4, 5])
>>> print(transition_matrix)

                0       1       2       3       4
---- group 0/4 ----
0       (       0       1       0       0       0               )       0
1       (       0.8     0       0.2     0       0               )       1
---- group 1/4 ----
2       (       0.9     0       0       0.1     0               )       2
---- group 2/4 ----
3       (       0       0       0       0       1               )       3
---- group 3/4 ----
4       (       0       0       0       1       0               )       4
---- group 4/4 ----
5       (       0       0       0       0       1               )       5
0       1       2       3       4



## Markovian States¶

In order to define which states have only one probability distribution over the successor states, we build a BitVector that contains the respective Markovian states:

[5]:

>>> markovian_states =  stormpy.BitVector(5, [1, 2, 3, 4])


## Building the Model¶

Now, we can collect all components:

[6]:

>>> components = stormpy.SparseModelComponents(transition_matrix=transition_matrix, state_labeling=state_labeling, markovian_states=markovian_states)
>>> components.choice_labeling = choice_labeling
>>> components.exit_rates = exit_rates


Finally, we can build the model:

[7]:

>>> ma = stormpy.storage.SparseMA(components)
>>> print(ma)

--------------------------------------------------------------
Model type:     Markov Automaton (sparse)
States:         5
Transitions:    8
Choices:        6
Markovian St.:  4
Max. Rate:      12
Reward Models:  none
State Labels:   2 labels
* init -> 1 item(s)