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.
First, we import Stormpy:
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.:
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:
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
Labeling¶
The labeling is similar the ones already covered in the previous examples.
state_labeling = stormpy.storage.StateLabeling(5)
state_labels = {"init", "deadlock"}
for label in state_labels:
state_labeling.add_label(label)
state_labeling.add_label_to_state("init", 0)
choice_labeling = stormpy.storage.ChoiceLabeling(6)
choice_labels = {"alpha", "beta"}
for label in choice_labels:
choice_labeling.add_label(label)
choice_labeling.add_label_to_choice("alpha", 0)
choice_labeling.add_label_to_choice("beta", 1)
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:
markovian_states = stormpy.BitVector(5, [1, 2, 3, 4])
Exit Rates¶
Lastly, we initialize a list to equip every (Markovian) state with an exit rate > 0:
exit_rates = [0.0, 10.0, 12.0, 1.0, 1.0]
Building the Model¶
Now, we can collect all components:
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:
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
* deadlock -> 0 item(s)
* init -> 1 item(s)
Choice Labels: 2 labels
* beta -> 1 item(s)
* alpha -> 1 item(s)
--------------------------------------------------------------