Motivation
To model systems that exhibit probabilistic behavior.
Markov Process
It is a stochastic process that satisfies Markov property.
MEMORYLESS: One can make predictions for the future of the process based only on its present state, independent of its future and past.
Classes of State-based Markov Models
| Deterministic | Non-deterministic | |
|---|---|---|
| Discrete time | Discrete-time Markov chains (DTMC) | Markov Decision Process (MDP), Probabilistic Automata(PA) |
| Continuous time | Continuous-time Markov chains (CTMC) | Continuous-time Markov Decision Process (CTMDP), Probabilistic Timed Automata (PTA) |
Determinism: there is only one set of transitions (sum of transitive probability is \(1\))
Non-determinism: there can be multiple sets of transitions (for each set, sum of transitive probability is \(1\)). "Different choices"
Continuous: Rate of making transition instead of probability.
DTMC
DTMC is a tuple \(D=(\mathcal S,s_{init},P)\) where
- \(\mathcal S\) is a finite set of states
- \(s_{init}\in\mathcal S\) is the initial state
- \(P:\mathcal S\times\mathcal S\to[0,1]\) is a transition probability matrix.
DTMC can have labeling function \(L:\mathcal S\to 2^{AP}\).
DTMC can have reward/cost function \(C:\mathcal S\times\mathcal S\to\mathbb R^{\geq 0}\), which maps pairs of states to non-negative real values. \(C(s,s')\) denotes the cost/reward when the transition from \(s\) to \(s'\) is taken.
Path
A path is a sequence of states that every transition has positive probability.
The probability of a path is the multiplication of the probabilities of all transitions in the path.
Cylinder set \(Cyl(\omega)\) for a finite path \(\omega\) is the set of infinite paths with the common finite prefix \(\omega\).
MDP
For each state, there might be multiple choices, adversary will choose one to decide how are transition probabilities.
An MDP is a tuple \((\mathcal S,s_{init},Steps,L)\) where
- \(Steps:\mathcal S\to 2^{Act\times Dist(\mathcal S)}\) is the probabilistic transition function where \(Act\) is the set of actions and \(Dists(\mathcal S)\) is the set of discrete probability distributions over \(\mathcal S\). Always be non-empty
- \(L\) is the labelling with atomic propositions
Adversary can be either memoryless (Always pick the same action on the same state) or not.
CTMC
Transition rate matrix assigns rates to each pair of states
- Used as a parameter to the exponential distribution.
- Transition between \(s\) and \(s'\) when \(R(s,s')>0\).
- Probability triggered before \(t\) time units: \(1e^{-R(s,s')t}\)
Race Conditions
If there exists multiple \(s'\) with positive rate, there will be a race condition.