Markov Chains Syntax

Example DTMC

The model below is an example of a Markov Chain model.

markov chain Model {
        A -- 1/2  -> B
        B -- 1/10 -> A
}

Syntax DTMC

Markov Chains are a graph-like structure and the discussion about syntax of graphs applies. The syntax of a Markov Chain always starts with markov chain <name> {. It ends with a closing curly bracket }. The core of the description of the DTMC is in the form of transitions S -- <p> --> T. Transitions are labelled with a probability that can be written as a fraction of integers, e.g., 2/3 or using decimal representation, such as 0.4.

State names are combinations of letters, numbers and the underscore character _ that start with a letter.

Self-transitions on states can be left implicit. If the total outgoing probability mass from a state is smaller than 1 and there is no self-transition in the model, then the remaining probability mass is assumed to be on an implicit self-transition.

States can optionally have annotations that are written between square brackets behind the state name, separated by semicolon, ;. There are two possible annotations: initial probability and reward.

• the initial probabilities defines the probability to initially be in the annotated state. The annotation is as follows: S[initial probability: <p>], where <p> is a probability as a rational fraction or in decimal notation. It can also be shortened as follows: [p: 1/4]. If the total specified initial probability mass is lower than 1, then the remaining probability mass is uniformly divided among the states without annotation of initial probability. In particular, if none of the states are annotated, a uniform initial distribution is assumed.
• the rewards annotation defines the reward gained when the state is visited. It is specified as follows: S [reward: 5]. The reward is an arbitrary positive or negative number specified as a rational fraction or a decimal number. The reward can be shortened as S[r: 1/3]. If no reward is specified for a state, it is assumed to be 0.