...

01-spec-and-impl.tex

@@ -232,7 +232,7 @@ Finally, deadlocks \textbf{does not display any behavior} -- that is, a $\delta$
                     \textbf{Algebraic structure} describes a set with additional properties -- e.g., an additive group over $\mathbb{N}$, a ring of integers modulo $x$, etc. 
                 }
                 \item {
-                    Two structures of the same \textbf{type} refers to structures with the same name -- e.g., two groups, two rings, etc. 
+                    Two \textbf{structures} of the same \textbf{type} refers to structures with the same name (i.e., class of property) -- e.g., two groups, two rings, etc. 
                 }
                 \item {
                     A \textbf{structure-preserving} map $f$ between two structures intuitively describes a structure such that, for properties $p \in X$, $q \in Y$ between same-type structures $X, Y$, any tuples $X^n \in p$ accepted by $p$ (e.g., $3 + 5 = 8 \implies (3, 5, 8) \in \mathbb{R}.(+)$) satisfies $\mathsf{map}(f, X^n) \in q$. 

02-semantic-equivalences.tex

@@ -16,12 +16,200 @@
 
 Define a lattice over which \textit{semantic equivalence relations} for spec. and impl. verification is defined.
 
+\begin{background}[reflexivity]
+    \begin{equation*}
+        \forall x \in X: x \circ x \iff \circ\ \mathrm{reflexive\ on}\ X
+    \end{equation*}
+\end{background}
+
+\begin{background}[symmetry]
+    \begin{equation*}
+        \forall x, y \in X:
+        \begin{prooftree}
+            \hypo{x \circ y}
+            \infer1{y \circ x}
+        \end{prooftree}
+        \iff \circ\ \mathrm{symmetric\ on}\ X
+    \end{equation*}
+\end{background}
+
+\begin{background}[transitivity]
+    \begin{equation*}
+        \forall x, y, z \in X: 
+        \begin{prooftree}
+            \hypo{x \circ y}
+            \hypo{y \circ z}
+            \infer2{x \circ z}
+        \end{prooftree}
+        \iff \circ\ \mathrm{transitive\ on}\ X
+    \end{equation*}
+\end{background}
+
+\begin{background}[equivalence relation]
+    \textbf{Equivalence relation} on set $X$ satisfies reflexivity, symmetry, and transitivity on $X$.
+\end{background}
+
 \begin{definition}[discrimination measure]
     One equivalence relation $\equiv$ is \textbf{finer} / \textbf{more discriminating} than another $\sim$ if each $\equiv$-eq. class is a subset of a $\sim$-eq. class. In other words,
     \begin{align*}
             \ &p \equiv q \implies p \sim q \\
         \iff\ &\equiv\ \mathrm{finer\ than}\ \sim
     \end{align*}
+
+    In other words, $\equiv$ creates finer partitions on its domain compared to $\sim$. 
 \end{definition}
 
+\paragraph*{Trace Equivalence}
+\begin{definition}[path]
+    A \textbf{path} of a process $p$ is an alternating sequence of states and transitions starting from state $p$. It can be infinite or ending in a state. 
+    
+    A path is \textbf{complete} if it is either infinite or ends in a state where no further transitions are possible -- a maximal path.
+\end{definition}
+
+\begin{definition}[complete trace]
+    A \textbf{complete trace} of process $p$ is the sequence of labels of transitions in a complete path. 
+    
+    The set of finite complete traces of process $p$ is denoted as ${CT}^{fin}(p)$, while the set of all finite/infinite complete traces of $p$ is ${CT}^{\infty}(p)$ -- aka. $CT(p)$ from now on.
+\end{definition}
+
+\begin{example}[${CT}^{\infty}$]
+    \begin{equation*}
+        {CT}^{\infty}(a.(\varepsilon + b.\delta)) = \{a\checkmark, ab\}
+    \end{equation*}
+\end{example}
+
+\begin{definition}[partial trace]
+    Likewise, a \textbf{partial trace} of a process $p$ is the sequence of labels of transitions in any partial path. 
+
+    We also likewise define ${PT}^{fin}(p)$ and ${PT}^{\infty}(p)$ for some process $p$. Define $PT(p)$ as ${PT}^{fin}(p)$. 
+\end{definition}
+
+\begin{definition}[$=_{PT}$]
+    Processes $p, q$ are \textbf{partial trace equivalent} ($p =_{PT} q$) if they have the same partial traces: 
+    \begin{equation*}
+        p =_{PT} q \iff PT(p) = PT(q)
+    \end{equation*}
+
+    Mirroring the differences between ${PT}^{fin}$ and ${PT}^{\infty}$, define \textbf{finitary partial trace equivalence} ($=_{{PT}^{fin}}$) and \textbf{infinitary partial trace equivalence} ($=_{{PT}^{\infty}}$).
+\end{definition}
+
+\begin{definition}[$=_{CT}$]
+    Processes $p, q$ are \textbf{complete trace equivalent} ($p =_{CT} q$) if \underline{moreover} they have the same complete traces: 
+    \begin{equation*}
+        p =_{CT} q \iff CT(p) = CT(q)
+    \end{equation*}
+
+    Mirroring the differences between ${CT}^{fin}$ and ${CT}^{\infty}$, define \textbf{finitary complete trace equivalence} ($=_{{CT}^{fin}}$) and \textbf{infinitary complete trace equivalence} ($=_{{CT}^{\infty}}$).
+\end{definition}
+
+\paragraph*{Weak Equivalences and $\tau$-actions}
+\begin{definition}[strong equivalence]
+    A \textbf{strong equivalence} relation treats $\tau$ like any other (observable) action. 
+
+    We assume above definitions for e.g., $=_{PT}$ to be assuming strong equivalence. 
+\end{definition}
+
+\begin{definition}[weak equivalence]
+    In its mirror case, a \textbf{weak equivalence} treats $\tau$ as if it is omitted from the input processes. 
+
+    We additionally define weak variants of the above 4 equivalences: $=_{{WPT}^{fin}}$, $=_{{WPT}^{\infty}}$, $=_{{WCT}^{fin}}$, $=_{{WCT}^{\infty}}$. 
+\end{definition}
+
+\paragraph*{Bisimulation Equivalence}
+\begin{definition}[bisimulation]
+    Let $A, P$ define the actions and predicates of an LTS (in addition to states, etc.). A \textbf{bisimulation} is a binary relation $\circ \subseteq S \times S$ satisfying: 
+    \begin{itemize}
+        \item $
+            s \circ t \implies 
+            (\forall p \in P: s \models p \iff t \models p)
+        $
+        \item $
+            s \circ t \wedge (\exists a \in A: s \xrightarrow{a} s^{'}) \implies
+            (\exists t^{'}: t \xrightarrow{a} t^{'}) \wedge s^{'} \circ t^{'}
+        $
+        \item $
+            s \circ t \wedge (\exists a \in A: t \xrightarrow{a} t^{'}) \implies
+            (\exists s^{'}: s \xrightarrow{a} s^{'}) \wedge s^{'} \circ t^{'}
+        $
+    \end{itemize}
+
+    Bisimulation (aka. \textbf{bisimulation equivalence}) is an equivalence relation. In general, bisimulation differentiates branching structure of processes.  
+\end{definition}
+
+\begin{definition}[bisimilarity]
+    Two states $s, t$ are bisimilar ($s \underline{\leftrightarrow} t$) if such a bisimulation $\circ$ exists between $s, t$.
+\end{definition}
+
+\begin{definition}[branching bisimulation]
+    Given $A, P$ upon LTS, weaken \underline{bisimulation} as follows: a \textbf{branching bisumlation} is a binary relation $\circ \subseteq S \times S$ satisfying: 
+    \begin{enumerate}
+        \item {$
+            s \circ t \wedge (\exists p \in P: s \models p) \implies
+            \exists t_1: t \rightsquigarrow t_1 \models p \wedge s \circ t_1
+        $ \label{def.bbeq.sat.1}}
+        \item {$
+            s \circ t \wedge (\exists p \in P: t \models p) \implies
+            \exists s_1: s \rightsquigarrow s_1 \models p \wedge s_1 \circ t
+        $ \label{def.bbeq.sat.2}}
+        \item {$
+        \begin{aligned}
+            &s \circ t \wedge (\exists a \in A_{\tau}: s \xrightarrow{a} s^{'}) \\
+            \implies &\exists t_1, t_2, t^{'}: t \rightsquigarrow t_1 \xrightarrow{(a)} t_2 = t^{'} \wedge s \circ t_1 \wedge s^{'} \circ t^{'}
+        \end{aligned}
+        $ \label{def.bbeq.sat.3}}
+        \item {$
+        \begin{aligned}
+            &s \circ t \wedge (\exists a \in A_{\tau}: t \xrightarrow{a} t^{'}) \\
+            \implies &\exists s_1, s_2, s^{'}: s \rightsquigarrow s_1 \xrightarrow{(a)} s_2 = s^{'} \wedge s_1 \circ t \wedge s^{'} \circ t^{'}
+        \end{aligned}
+        $ \label{def.bbeq.sat.4}}
+    \end{enumerate}
+    where: 
+    \begin{itemize}
+        \item $
+        \begin{aligned}
+            &s \rightsquigarrow s^{'}  \\
+            \iff &\exists n \ge 0: \exists s_0, \dots, s_n: 
+            s = s_0 \xrightarrow{\tau} \dots \xrightarrow{\tau} s_n = s^{'}
+        \end{aligned}
+        $
+        \item $
+            A_{\tau} \coloneq A \cup \{\tau\}
+        $
+        \item $
+            s \xrightarrow{(a)} s^{'} \coloneq 
+            \begin{cases*}
+                s \xrightarrow{a} s^{'}                   & if $a \in A$ \\
+                s \xrightarrow{\tau} s^{'} \vee s = s^{'} & if $a = \tau$
+            \end{cases*}
+        $
+    \end{itemize}
+
+    Two processes $p, q$ are branching bisimilar ($p \underline{\leftrightarrow}_{b} t$) if such a binary relation $\circ$ exists.
+\end{definition}
+
+\begin{definition}[delay bisimulation]
+    Given $\underline{\leftrightarrow}_{b}$, drop requirements $s \circ t_1$ and $s_1 \circ t$, thus producing $\underline{\leftrightarrow}_{d}$.
+\end{definition}
+
+\begin{definition}[weak bisimulation]
+    Given $\underline{\leftrightarrow}_{b}$, 
+    \begin{itemize}
+        \item Drop requirements $s \circ t_1$, $s_1 \circ t$; 
+        \item Relax $t_2 = t^{'}$ and $s_2 = s^{'}$ to $t_2 \rightsquigarrow t^{'}$ and $s_2 \rightsquigarrow s^{'}$, respectively.
+    \end{itemize}
+    Thus producing $\underline{\leftrightarrow}_{w}$.
+\end{definition}
+
+\paragraph*{Language Equivalence} This paragraph is moved here for ergonomics.
+\begin{definition}[language equivalence]
+    Processes $p, q$ are \textbf{language equivalent} if they have the same traces leading to terminating states -- i.e., equal subset of terminating partial traces. 
+
+    Intuitively (and indeed) this is coarser than partial trace equivalence. 
+\end{definition}
+
+\paragraph*{Overview: The Hasse Diagram}
+\dots
+
+
 \end{document}

03-ccs.tex

@@ -0,0 +1,137 @@
+\documentclass[99-notes-packed.tex]{subfiles}
+
+\begin{document}
+\paragraph*{CCS}
+Define the set of operations and semantics: 
+\begin{itemize}
+    \item {
+        $0$ (inaction): 
+        
+        $0$ represents a graph with 1 (initial) state, 0 transitions.
+    }
+    \item {
+        $a, \bar{a}$ (complementary actions): 
+
+        Complementary actions are assumed to communicate / synchronize with one another. 
+    }
+    \item {
+        $a.P$ (action prefix) for each action $a$, process $P$, which:  
+        \begin{enumerate}
+            \item Define new initial state $\mathsf{i}$.
+            \item Creates transition $\mathsf{i} \xrightarrow{a} I_P$.
+        \end{enumerate}
+    }
+    \item {
+        $P + Q$ (summation / choice / alternative composition), where: 
+        \begin{itemize}
+            \item Define new initial state $\mathsf{root}$.
+            \item $\mathrm{States}(P + Q) \coloneqq \mathrm{States}(P) \cup \mathrm{States}(Q) \cup \{\mathsf{root}\}$
+            \item Replace all $I_P \xrightarrow{a} s$ with $\mathsf{root} \xrightarrow{a} s$. 
+            \item Replace all $I_Q \xrightarrow{a} s$ with $\mathsf{root} \xrightarrow{a} s$.
+        \end{itemize}
+    }
+    \item {
+        $P | Q$ (parallel composition).
+
+        This takes the cartesian product of the states of $P, Q$, such that: 
+        \begin{itemize}
+            \item $s \xrightarrow{a} s^{'} \in P \implies \forall t \in Q: (s, t) \xrightarrow{a} (s^{'}, t)$
+            \item $t \xrightarrow{a} t^{'} \in Q \implies \forall s \in P: (s, t) \xrightarrow{a} (s, t^{'})$
+            \item $(s \xrightarrow{a} s^{'} \in P) \wedge (t \xrightarrow{\bar{a}} t^{'} \in Q) \implies (s, t) \xrightarrow{\tau} (s^{'}, t^{'})$
+        \end{itemize}
+
+        Note that \textbf{CCS adheres strictly to a handshaking communication format} -- this differs from ACP which gives greater leeway to implementation, via the use of $\gamma$ operator.
+    }
+    \item {
+        $P{\backslash}a$ (restriction) for each action $a$. 
+
+        This produces copy of $P$ such that all actions $a, \bar{a}$ are omitted. This is useful to remove unsuccessful communication. 
+    }
+    \item {
+        $P[f]$ (relabelling) for each function $f: A \rightarrow A$.
+
+        This replaces each label $a, \bar{a}$ by $f(a), \overline{f(a)}$.
+    }
+\end{itemize}
+
+\paragraph*{Recursion}
+\begin{definition}[process names and expressions]
+    Suppose we bind names $X, Y, Z, \dots$ to some expression in the CCS language: 
+    \begin{equation*}
+        X = P_X
+    \end{equation*}
+    Here, $P_X$ represents ANY expression in the language, possibly including $X$. 
+
+    It is trivial to see this can cause recursive definitions: 
+    \begin{equation*}
+        X = a.X
+    \end{equation*}
+\end{definition}
+
+\begin{definition}[recursive specification]
+    Define \textbf{recursive specification} as partial function $s: X \rightarrow E$: 
+    \begin{itemize}
+        \item $X$: \textbf{recursion variables}. 
+        \item $E$: \textbf{recursion equations} of form $x = P_x$.
+    \end{itemize}
+
+    In general, recursive spec.s are written as follows: 
+    \begin{equation*}
+        \langle x | s \rangle
+    \end{equation*}
+    which reads as ``process $x$ satisfying equation $s$''. 
+\end{definition}
+
+\begin{definition}[guarded recursion]
+    A recursion is \textbf{guarded} if each occurrence of a process name in $P_X$ occurs within the scope of a subexpression $a.P^{'}_X$. 
+    
+    Think of it as being unwind-able such that progress is guaranteed.
+\end{definition}
+
+\paragraph*{Structural Operational Semantics (CCS)}
+\begin{center}
+    \begin{tabular}{cc}
+        $
+        \begin{prooftree}
+            \infer0{a.E \xrightarrow{a} E}
+        \end{prooftree}
+        $   &
+        $
+        \begin{prooftree}
+            \hypo{E_j \xrightarrow{a} E_j^{'}}
+            \infer1{\sum_{i \in I}E_i \xrightarrow{a} E_j^{'}}
+        \end{prooftree}\ (j \in I)
+        $   \\
+        \\
+        $
+        \begin{prooftree}
+            \hypo{E \xrightarrow{a} E^{'}}
+            \infer1{E | F \xrightarrow{a} E^{'} | F}
+        \end{prooftree}
+        $   &
+        $
+        \begin{prooftree}
+            \hypo{E \xrightarrow{a} E^{'}}
+            \hypo{F \xrightarrow{\overline{a}} F^{'}}
+            \infer2{E | F \xrightarrow{\tau} E^{'} | F^{'}}
+        \end{prooftree}
+        $   \\
+        \\
+        $
+        \begin{prooftree}
+            \hypo{E \xrightarrow{a} E^{'}}
+            \hypo{a \notin L \cup \overline{L}}
+            \infer2{E{\backslash}L \xrightarrow{a} E^{'}{\backslash}L}
+        \end{prooftree}
+        $   &
+        $
+        \begin{prooftree}
+            \hypo{E \xrightarrow{a} E^{'}}
+            \infer1{E[f] \xrightarrow{f(a)} E^{'}[f]}
+        \end{prooftree}
+        $   \\
+        \\
+    \end{tabular}
+\end{center}
+
+\end{document}

04-congruence.tex

@@ -0,0 +1,116 @@
+\documentclass[99-notes-packed.tex]{subfiles}
+
+\begin{document}
+\paragraph*{Congurence}
+If an equivalence relation is a \textit{congurence} for an operator -- i.e., an operator is \textit{compositional} for the equivalence -- then there exists a sort of isomorphism detailed as follows: 
+
+\begin{definition}[congurence]
+    An equivalence $\sim$ is a \textbf{congruence} for a language $\mathcal{L}$ if: 
+    \begin{equation*}
+        \forall C[\ ] \in \mathcal{L}: P \sim Q \implies C[P] \sim C[Q]
+    \end{equation*}
+    where: 
+    \begin{itemize}
+        \item $C[\ ]$ (context) represents a $\mathcal{L}$-expression with a hole in it, plugged (e.g., with $P$) as $C[P]$. 
+    \end{itemize}
+    
+    For example, let $P = a.[\ ]$: 
+    \begin{equation*}
+        \begin{prooftree}
+            \hypo{P = Q}
+            \infer1{a.P = a.Q}
+        \end{prooftree}
+    \end{equation*}
+    Equivalently, we can say that $CCP.(.)$ is compositional under equality ($=$). 
+\end{definition}
+
+\begin{example}[$=_{CT}$ and $\partial_{H}$]
+    This is a counterexample for showing why $=_{CT}$ is NOT a congurence over ACP. Obviously: 
+    \begin{equation*}
+        a.b + a.c =_{CT} a.(b + c)
+    \end{equation*}
+
+    However: 
+    \begin{equation*}
+        \partial_{\{c\}}(a.b + a.c) \neq_{CT} \partial_{\{c\}}(a.(b + c))
+    \end{equation*}
+\end{example}
+
+\begin{definition}[congurence closure]
+    A \textbf{congurence closure} $\sim^c$ of $\sim$ wrt. language $\mathcal{L}$ is defined by: 
+    \begin{equation*}
+        P \sim^{c} Q \iff \forall C[\ ] \in \mathcal{L}: C[P] \sim C[Q]
+    \end{equation*}
+\end{definition}
+
+\paragraph*{Equational Axiomisation}
+In terms of e.g., real addition we describe the operator as possessing e.g., associativity and commutativity, which in turn allows us to do some transformation during analysis, etc. 
+
+Same goes for operators in e.g, CCS: 
+\begin{center}
+    \begin{tabular}{cc}
+        $(P + Q) + R = P + (Q + R)$ & (associativity) \\
+        $P + Q = Q + P$ & (commutativity) \\
+        $P + P = P$ & (idempotence) \\
+        $P + 0 = P$ & ($0$ as neutral element of $+$)
+    \end{tabular}
+\end{center}
+
+\begin{definition}[CCS: expansion theorem]
+    Suppose: 
+    \begin{align*}
+        P \coloneqq& \sum_{i \in I} a_i.P_i \\
+        Q \coloneqq& \sum_{j \in J} b_i.Q_j
+    \end{align*}
+
+    Then, 
+    \begin{align*}
+        P | Q &= \sum_{i \in I} a_i(P_i | Q) \\
+              &+ \sum_{i \in I, j \in J} \tau(P_i | Q_j)\ (\mathrm{given\ }a_i = \overline{b_j}) \\
+              &+ \sum_{j \in J} b_i(P | Q_j)
+    \end{align*}
+
+    Expressions of the form $\sum a.P$ are aka. \textbf{head normal form}.
+\end{definition}
+
+\begin{definition}[Recursive Definition Principle]
+    \begin{equation*}
+        i \in [1, n]: \langle X_i | E \rangle \in \mathsf{Expr}(X_1 \coloneqq \langle X_1 | E \rangle, \dots, X_n \coloneqq \langle X_n | E \rangle)
+    \end{equation*}
+
+    Basically, some series of expressions for $X_1, \dots, X_n$ exists as solution for $E$. 
+\end{definition}
+
+\begin{definition}[Recursive Specification Principle]
+    If there \underline{exists}
+    \begin{equation*}
+        i \in [1, n]: y_i \leftarrow \mathsf{Expr}(y_1, \dots, y_n)
+    \end{equation*}
+    then: 
+    \begin{equation*}
+        i \in [1, n]: y_i = \langle X_i | E \rangle
+    \end{equation*}
+
+    In other words, any $y_{1 \dots n}$ that exists is the sole solution for $E$ modulo bisimulation equivalence. 
+\end{definition}
+
+\paragraph*{Rooted Bisimilarity}
+We note that depending on semantics of $\mathcal{L}$, equivalences may (and in fact likely) fail to be a congurence over $\mathcal{L}$. This also is the case for e.g., branching bisimilarity: $\tau.a =_{BB} a$ but $\tau.a + b \ne_{BB} a + b$. 
+
+ACP and CCS fixes this by changing the equivalence operator. 
+
+\begin{definition}[Rooted Branching Bisimilarity]
+    \begin{align*}
+        P =_{rBB} Q \iff &(P \xrightarrow{a} P^{'} \implies Q \xrightarrow{a} Q^{'} \wedge P^{'} =_{BB} Q^{'})\ \wedge \\
+        &(Q \xrightarrow{a} Q^{'} \implies P \xrightarrow{a} P^{'} \wedge P^{'} =_{BB} Q^{'})
+    \end{align*}
+\end{definition}
+
+\begin{definition}[Rooted Weak Bisimilarity]
+    \begin{align*}
+        P =_{rWB} Q \iff &(P \xrightarrow{a} P^{'} \implies Q \xrightarrow{a} Q^{'} \wedge P^{'} =_{WB} Q^{'})\ \wedge \\
+        &(Q \xrightarrow{a} Q^{'} \implies P \xrightarrow{a} P^{'} \wedge P^{'} =_{WB} Q^{'})
+    \end{align*}
+\end{definition}
+
+\end{document}

99-notes-packed.tex

@@ -2,7 +2,8 @@
 
 \usepackage[utf8]{inputenc}
 \usepackage[T1]{fontenc}
-\usepackage[a4paper, margin=1cm]{geometry}
+\usepackage[a4paper, margin=0.25cm, landscape]{geometry}
+
 
 \usepackage{multicol}                       % 2-col formatting
 \usepackage{hyperref}
@@ -21,19 +22,23 @@
 
 % environment `definition` prints as "Definition" and has counter reset per section.
 \newtheorem{definition}{Definition}[section]
-
 \newtheorem{background}{Background}[section]
+\newtheorem{example}{Example}[section]
 
 \begin{document}
+\begin{multicols*}{3}
 
 \section{LTS; ACP}
-\begin{multicols*}{2}
 \subfile{01-spec-and-impl}
-\end{multicols*}
 
 \section{Semantic Equivalences}
-\begin{multicols*}{2}
 \subfile{02-semantic-equivalences}
-\end{multicols*}
 
+\section{CCS; SOS}
+\subfile{03-ccs.tex}
+
+\section{Equational Axiomisation}
+\subfile{04-congruence.tex}
+
+\end{multicols*}
 \end{document}