diff --git a/MoPro Cheatsheet.pdf b/MoPro Cheatsheet.pdf
index 2282e3ea5fb85ff00c1342feea8289c021e47f1e..314fa6496eb7b595401503de84b538eded4b340f 100644
Binary files a/MoPro Cheatsheet.pdf and b/MoPro Cheatsheet.pdf differ
diff --git a/MoPro Cheatsheet.tex b/MoPro Cheatsheet.tex
index 2a5351f3beca866acd0f33f6286abba86bbd22af..1de1f74d0800a17fde3fa56795bb7ebbae593b8c 100644
--- a/MoPro Cheatsheet.tex	
+++ b/MoPro Cheatsheet.tex	
@@ -211,7 +211,7 @@ The probability that a state satisfies the property is the reachability probabil
 \subsection{$\omega$-regular properties}
 An $\omega$-regular expression is composed of finite prefixes followed by infinite repetitions of of finite words, i. e. $x_1\cdot y_1^\omega+x_2\cdot y_2^\omega+\ldots$. Note that the repeated part cannot be empty. An LT property is $\omega$-regular, if there it can be characterized using an $\omega$-regular expression.
 
-Deterministic Blüchi automata (DBAs) capture a subset of $\omega$-regular properties. Since it considers infinite runs, the acceptance condition differs from DFAs. A DBA accepts a run, if the run visits its final states infinitely often. The language of any DBA is $\omega$-regular, but not all $\omega$-regular languages can be described as DBAs.\sidenote{DBAs recognize the limit language of a regular language.}
+Deterministic Büchi automata (DBAs) capture a subset of $\omega$-regular properties. Since it considers infinite runs, the acceptance condition differs from DFAs. A DBA accepts a run, if the run visits its final states infinitely often. The language of any DBA is $\omega$-regular, but not all $\omega$-regular languages can be described as DBAs.\sidenote{DBAs recognize the limit language of a regular language.}
 
 Deterministic Rabin automata (DRAs) are $\omega$-regular. Their final states are pairs of sets, and a run is accepted, if for some final state pair $(L,K)$ the set $L$ is visited only finitely often, and $K$ is visited infinitely often.\sidenote{A DBA is a DRA with a final state pair of the form $\{(\emptyset, F)\}$.}
 
@@ -251,6 +251,26 @@ The probability for the unbounded until operator $\Phi\U\Psi$ can be determined
 
 The time complexity of PCTL model checking is polynomial in the size of $\D$, and linear in the biggest $n$ in a bounded until and the size of the formula. Stopping the convergence when two iterations differ less than a threshold is unsound.\sidenote{When the convergence is slow, the iteration will be stopped too early. There is no guarantee to be close to the actual value with unsound iteration.} This can be handled by lower and upper bounds. The error is $Pr(\lozenge G)-Pr(\lozenge^{\leq k}G)$, i. e. the probability to reach $G$ in more than $k$ steps. That is less than $Pr(\square^{\leq k}S_?)\cdot\max_{s\in S_?}Pr(\lozenge G)$, but more than $Pr(\square^{\leq k}S_?)\cdot\min_{s\in S_?}Pr(\lozenge G)$.
 
+\subsection{Qualitative PCTL}
+Removing bounded until and only allowing the bounds $>1$ and $=0$\sidenote{The bounds $=1$ and $>0$ can be derived from these.} yields qualitative PCTL. Computation tree logic (CTL, without P) has the $\exists$- and $\forall$-operators instead of $\P$. A PCTL formula $\Phi$ is equivalent to a CTL formula $\Psi$, if $Sat(\Phi)=Sat(\Psi)$ for all DTMCs. Example equivalences include $\P_{>0}(\lozenge a)\equiv \exists\lozenge a$ and $\P_{=1}(\square a)\equiv \forall\square a$, but note that $\P_{>0}(\square a)\not\equiv\exists\square a$ and $\P_{=1}(\lozenge a)\not\equiv\forall\lozenge a$.
+
+Qualitative PCTL and CTL have incomparable expressive power, i. e. some PCTL formulae are not expressible in CTL and vice versa.\sidenote{This only holds in general, as for finite DTMCs $\P_{=1}(\lozenge a)\equiv \forall((\exists\forall a)\operatorname{W}a)$ where $\Phi\operatorname{W}\Psi:=(\Phi\U\Psi)\lor \square\Phi$ is the weak until operator.} Almost sure reachability is not expressible in CTL, i. e. there is no equivalent for $\P_{=1}(\lozenge a)$ or $\P_{>0}(\square a)$. On the other hand, there is no qualitative PCTL equivalent for $\forall\lozenge a$ or $\exists\square a$. The difference is that CTL only characterizes the underlying graph, while qualitative PCTL takes the probabilities into account, but cannot ignore them.
+
+However, in finite DTMCs the two logics can be made equally expressive by requiring fairness. In a fair path, when a state is visited infinitely often, all of its successors are also visited infinitely often. Fair CTL only considers fair paths for $\exists$ and $\forall$, i. e. paths that do not satisfy the operator, but are unfair, are ignored. Qualitative PCTL and fair CTL are equally expressive for finite Markov chains.
+
+Almost-sure repeated reachability and similar probabilities are definable in qualitative PCTL by nesting $\P$-operators, e. g. $s\models \P_{=1}(\square\P_{=1}(\lozenge G)) \iff Pr\{\pi\in Paths(s) \mid \pi\models\square\lozenge G\}=1$.
+
+\section{Bisimulation}
+A strong bisimulation is a relation\sidenote{Not every strong bisimulation is an equivalence relation, because it might not be transitive.} between two labeled transition systems (LTS), such as DTMCs. The relation associates states from the two LTSs in a way that the labels correspond and that the transitions always end up in equivalent states.\sidenote{There are two ways to define strong bisimulation.} Two LTSs are strongly bisimilar, if there exists a bisimulation. The quotient of an LTS is the reduction to its equivalence classes under bisimulation.
+
+Probabilistic bisimulation is an equivalence relation\sidenote{In contrast to strong bisimulation, probabilistic bisimulation is always an equivalence relation.} requires that two bisimilar states have the same probability to move to each equivalence class. Even though there might be different amounts of transitions, the sums of those ending up in the same equivalence class should be equal. Two DTMCs are bisimilar, if each equivalence class has equal initial probability in each DTMC.
+
+Bisimulation preserves PCTL in the sense that two bisimilar states are always equivalent under PCTL, i. e. there is no PCTL formula that can distinguish the states. There is an extension, PCTL$^*$, and a reduced form PCTL$^-$ that have the same property. PCTL$^*$ allows mixing of state and path formulae, while PCTL$^-$ only has disjunction, conjunction, and a upper-bounded $\P_{\leq p}$ operator. Probabilistic bisimulation coincides with the notion of lumpability, as it is the coarsest possible lumpable partition.
+
+The strategy to build a DTMC's quotient under probabilistic bisimulation is to put all nodes with the same label into an equivalence class. Then all outgoing transitions from supposedly equivalent states are checked to land in the same equivalence class. If there is a case where a state has a transition to an equivalence class that other supposedly equivalent states lack, then this equivalence class must be divided into two. This is repeated until bisimilarity is achieved.
+
+\todo{Improve description.}
+
 \clearpage
 \printbibliography