53 lines
No EOL
2 KiB
TeX
53 lines
No EOL
2 KiB
TeX
\documentclass[99-notes-packed.tex]{subfiles}
|
|
|
|
\begin{document}
|
|
\paragraph*{Preorder}
|
|
Remember equivalence? Meet its lesser sibling, preorder:
|
|
|
|
\begin{definition}[Preorder]
|
|
A \textbf{preorder} ($\sqsubseteq$) denotes a \underline{transitive, reflexive} relation on a set.
|
|
|
|
Crucially, preorder is \underline{NOT symmetrical} compared to equivalence.
|
|
|
|
For example, $\le$ is a preorder over $\mathbb{R}$ (in fact, a partial-order).
|
|
\end{definition}
|
|
|
|
We define preorders in relation of equivalences already defined in this course. For example, partial trace preorder $\sqsubseteq_{PT}$:
|
|
\begin{equation*}
|
|
P \sqsubseteq_{PT} Q \iff PT(P) \supseteq PT(Q)
|
|
\end{equation*}
|
|
where $Q$ becomes a \textbf{refinement} of $P$ -- all properties of $P$ must hold for $Q$, while $Q$ can hold more properties than $P$.
|
|
|
|
In general, we want to prove:
|
|
\begin{equation*}
|
|
\mathrm{Spec} \sqsubseteq_{\sim} \mathrm{Impl}
|
|
\end{equation*}
|
|
|
|
\begin{definition}[Kernel]
|
|
For each preorder $\sqsubseteq_{\sim}$ there exists an associated equivalence relation $\equiv_{\sim}$:
|
|
\begin{equation*}
|
|
P \equiv Q \iff P \sqsubseteq Q \wedge Q \sqsubseteq P
|
|
\end{equation*}
|
|
If this holds, $P, Q$ are \textbf{kernels} of each other.
|
|
\end{definition}
|
|
|
|
\paragraph*{Simulation}
|
|
A \textbf{simulation} relation expresses a preorder between two processes $P, Q$ such that:
|
|
\begin{equation*}
|
|
P \sqsubseteq_{S} Q \iff \forall (P \xrightarrow{a} P^{'}): \exists (Q \xrightarrow{a} Q^{'}): P^{'} \sqsubseteq_{S} Q^{'}
|
|
\end{equation*}
|
|
|
|
Using definitions for general preorders, define \textbf{simulation equivalence} as follows:
|
|
\begin{equation*}
|
|
P \equiv_{S} Q \iff P \sqsubseteq_{S} Q \wedge Q \sqsubseteq_{S} P
|
|
\end{equation*}
|
|
|
|
\begin{example}[$\equiv_{S}$ vs. $=_{B}$]
|
|
Simulation equivalence is NOT equivalent to bisimulation. Case in point:
|
|
\begin{align*}
|
|
P &\coloneqq a.b + a.(b + c) \\
|
|
Q &\coloneqq a.(b + c)
|
|
\end{align*}
|
|
\end{example}
|
|
|
|
\end{document} |