...

04-congruence.tex

@@ -58,10 +58,12 @@ Same goes for operators in e.g, CCS:
 
 \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*}
+    \begin{center}
+        \begin{tabular}{cc}
+            $P \coloneqq \sum_{i \in I} a_i.P_i$ &
+            $Q \coloneqq \sum_{j \in J} b_i.Q_j$
+        \end{tabular}
+    \end{center}
 
     Then, 
     \begin{align*}
@@ -97,20 +99,64 @@ Same goes for operators in e.g, CCS:
 \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. 
-
+ACP and CCS fixes this by changing the equivalence operator. CSP fixes this by foregoing the $+$ 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*}
+
+    $=_{rBB}$ is equivalent to branching bisimulation congruence $=_{BB}^c$ over ACP.
 \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^{'})
+        P =_{rWB} Q \iff &(P \xrightarrow{a} P^{'} \implies Q \xrightarrow{\tau \ast a \tau \ast} Q^{'} \wedge P^{'} =_{WB} Q^{'})\ \wedge \\
+        &(Q \xrightarrow{a} Q^{'} \implies P \xrightarrow{\tau \ast a \tau \ast} P^{'} \wedge P^{'} =_{WB} Q^{'})
     \end{align*}
+
+    $=_{rWB}$ is equivalent to weak bisimulation congruence $=_{WB}^c$ over CCS.
+\end{definition}
+
+\begin{definition}[Eq. axiomisation for rBB, rWB] 
+    $=_{rWB}$ is axiomatised as follows: 
+    \begin{align}
+        a.\tau.P &= a.P \\
+        \tau.P &= \tau.P + P \\
+        a.(\tau.P + Q) &= a.(\tau.P + Q) + a.P
+    \end{align}
+
+    $=_{rBB}$ is axiomatised as follows: 
+    \begin{equation*}
+        a.(\tau.(P + Q) + Q) = a.(P + Q)
+    \end{equation*}
+\end{definition}
+
+\paragraph*{Strongly/Weakly Guarded Recursions}
+Recall that a recursive spec of the form e.g. $X = a.(b + X)$ is guarded -- $X$ exists as a subexpression of $X$ -- and are equivlent modulo strong bisimilarity (viz. RSP). 
+
+On the other hand $X = \tau.X$ has solely equivalent solutions modulo $=_{B}$ but not up to e.g. $=_{rBB}$. This breaks the equivalence lattice -- we hence need a stronger concept of \underline{unguardedness} for $=_{B}$.
+
+\begin{definition}[strong unguardedness]
+    A \textbf{strongly unguarded} recursive specification is one where, for
+    \begin{equation*}
+        X = \mathsf{Expr}(X, \dots)
+    \end{equation*}
+    the recursive variable $X$ occurs NOT in a subterm of the form: 
+    \begin{equation*}
+        a \leftarrow A \cup \{\tau\}: a.P^{'}, X \in P^{'}
+    \end{equation*}
+    as in, $X$ is not guarded by $\forall a \in A$ nor $\tau$. 
+
+    It turns out that \textbf{RSP is sound modulo bisimulation for all non-strongly-unguarded recursive specifications}. 
+\end{definition}
+
+\begin{definition}[weak unguardedness]
+    Likewise, a \textbf{weakly unguarded} recursive specification is one where recursive variable $X$ is NOT guarded by $\forall a \in A$ only. 
+
+    Note that strong unguardedness entails weak unguardedness.
+
+    \textbf{RSP is sound modulo weak/branching bisimulation for all non-weakly-unguarded recursive specifications}. 
 \end{definition}
 
 \end{document}

05-csp.tex

@@ -0,0 +1,91 @@
+\documentclass[99-notes-packed.tex]{subfiles}
+
+\begin{document}
+\paragraph*{CSP}
+Introduce the following operations: 
+\begin{enumerate}
+    \item {
+        $0$ or $\mathsf{STOP}$ (inaction).
+
+        Likewise CCS, a graph with 1 (initial) state, 0 transitions. 
+    }
+    \item {
+        $a.P$ or $a \rightarrow P$ (action prefix) for $\forall a \in A$. 
+
+        Likewise CCS.
+    }
+    \item {
+        $P \square Q$ (external choice). 
+
+        Semantically it is similar to parallel composition without synchronization, where: 
+        \begin{itemize}
+            \item {
+                Prior to ``choice'', one of the two actions might happen between the processes.
+            }
+            \item {
+                After one of the action happens, only the choiced process may occur at runtime. 
+            }
+        \end{itemize}
+    }
+    \item {
+        $P \sqcap Q$ (internal choice):
+        \begin{equation*}
+            \mathrm{CSP}[P \sqcap Q] \equiv \mathrm{CCS}[\tau.P + \tau.Q]
+        \end{equation*}
+    }
+    \item {
+        $P {||}_{S} Q$ (parallel composition) with enforced synchronization over $S \subseteq A$. Semantically speaking: 
+        \begin{itemize}
+            \item $
+                \mathsf{States}(P {||}_{S} Q) \coloneqq
+                \mathsf{States}(P) \times \mathsf{States}(Q)
+            $
+            \item {
+                $(s, t) \xrightarrow{a} (s^{'}, t)$ if 
+                $(a \notin S) \wedge (s \xrightarrow{a} s^{'} \in P)$
+            }
+            \item {
+                $(s, t) \xrightarrow{a} (s, t^{'})$ if 
+                $(a \notin S) \wedge (t \xrightarrow{a} t^{'} \in Q)$
+            }
+            \item {
+                $(s, t) \xrightarrow{a} (s^{'}, t^{'})$ if 
+                $(a \in S) \wedge (s \xrightarrow{a} s^{'} \in P) \wedge (t \xrightarrow{a} t^{'} \in Q)$
+            }
+        \end{itemize}
+    }
+    \item {
+        $P/a$ (concealment).
+
+        Like CCS, rename $a$ into $\tau$. 
+    }
+    \item {
+        $P[f]$ (renaming) for $f \in (A \rightarrow A)$
+
+        Likewise CCS.
+    }
+\end{enumerate}
+
+Weak and branching bisimulation are congurences for CSP.
+
+\paragraph*{GSOS}
+As a general form over languages, GSOS describes a transition rule of the following form: define 
+\begin{itemize}
+    \item {
+        $\Sigma$ be the collection of function symbols wrt. a language. 
+    }
+    \item {
+        $\mathsf{arity}: \Sigma \rightarrow \mathbb{N}$ a function exposing the arity of the function symbol in question.
+    }
+\end{itemize}
+then, under GSOS semantics, the language could be expressed as follows: 
+\begin{equation*}
+    \begin{prooftree}
+        \hypo{x_i \xrightarrow{a} y_i, \dots\ (f \in \Sigma, i \in [1, \mathsf{arity}(f)], y_i \notin \mathsf{args}(f))}
+        \infer1{f(x_1, \dots, x_{\mathsf{arity}(f)}) \xrightarrow{a} \mathsf{Expr}(x_1, \dots, x_{\mathsf{arity}(f)}, y_i, \dots)}
+    \end{prooftree}
+\end{equation*}
+
+It is the generalization of SOS rules we have covered earlier.
+
+\end{document}

06-hml.tex

@@ -0,0 +1,28 @@
+\documentclass[99-notes-packed.tex]{subfiles}
+
+\begin{document}
+\paragraph*{HML}
+Let $\varphi, \psi$ be HML expressions: 
+\begin{equation*}
+    \varphi, \psi \Coloneqq 
+    \top\ |\ \bot\ |\ \neg \varphi\ |\ \varphi \wedge \psi\ |\ 
+    \varphi \vee \psi \ |\ \langle A\rangle \Phi \ |\ [A] \Phi
+\end{equation*}
+where $\Phi$ denotes predicates. 
+
+We omit explanation of familiar syntactic elements from FOL. Besides them: 
+\begin{align*}
+    P \models [A]\Phi &\iff 
+    \forall Q: (\exists a \in A: P \xrightarrow{a} Q) \implies (Q \models \Phi) \\
+    P \models \langle A\rangle \Phi &\iff 
+    \exists Q: \exists a \in A: P \xrightarrow{a} Q \wedge Q \models \Phi
+\end{align*}
+
+\begin{example}[deadlock in HML]
+    Given set of all actions $A$, a process $P$ deadlocks if this holds:  
+    \begin{equation*}
+        P \models [A]\bot
+    \end{equation*}
+\end{example}
+
+\end{document}

07-preorder.tex

@@ -0,0 +1,53 @@
+\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}

08-ltl-ctl-kripke.tex

@@ -0,0 +1,101 @@
+\documentclass[99-notes-packed.tex]{subfiles}
+
+\begin{document}
+\paragraph*{LTL}
+Let $\phi, \psi$ be LTL expressions, $p \in AP$ an atomic predicate, $\rightarrow^\ast$ indicating 0 or more steps (like regex):
+\begin{align*}
+    \phi, \psi \Coloneqq&\ p\ |\ \top\ |\ \bot\ |\ \phi \wedge \psi\ |\ \phi \vee \psi\ |\ \neg \phi\ |\ \phi \implies \psi \\
+    |&\ X \phi: 
+        \pi \models X \phi \iff 
+        \exists {\pi}^{'}: \pi \rightarrow {\pi}^{'} \models \phi \\
+    |&\ F \phi: 
+        \pi \models F \phi \iff
+        \exists {\pi}^{'}: \pi \rightarrow^\ast {\pi}^{'} \models \phi \\
+    |&\ G \phi: 
+        \pi \models G \phi \iff
+        \forall {\pi}^{'}: (\pi \rightarrow^\ast {\pi}^{'}) \implies ({\pi}^{'} \models \phi) \\ 
+    |&\ \phi U \psi: \pi_0 \models \phi U \psi \\
+     &  \iff \exists \pi_0 \rightarrow^\ast P \models \psi: \forall \pi_i \in \pi_0 \rightarrow^\ast \pi_N \rightarrow \Pi: \pi_i \models \phi \\
+    |&\ \phi W \psi: 
+        \pi \models \phi W \psi \iff \pi \models (\phi U \psi) \vee (G \phi)
+\end{align*}
+
+\paragraph*{CTL}
+Orthogonally (in terms of expressibility), CTL prefixes all $X | F | G | U$ operators with temporal signifiers: 
+\begin{align*}
+    A \sim \forall&:\ \textrm{for all paths} \\
+    E \sim \exists&:\ \textrm{exists some path} 
+\end{align*}
+
+\begin{example}[incomparability of CTL, LTL]
+    No LTL equivalent exists for CTL formula $AG(EF a)$. Likewise, no CTL equivalent exists for LTL formula $F(G a)$. 
+\end{example}
+
+\paragraph*{Kripke Structure} is an alternative means of representing a transition system. Let $AP$ be a set of atomic predicates. A Kripke structure over $AP$ is a tuple $(S, \rightarrowtriangle, \models)$ where: 
+\begin{itemize}
+    \item $S$: set of state.
+    \item $\rightarrowtriangle \subseteq S \times S$: transition relation. 
+    \item $\models \subseteq S \times AP$: state-predicate mapping. 
+\end{itemize}
+
+LTL and CTL operate upon Kripke structures. 
+
+A state $s \models \phi$ if for all paths incident from $s$, each path satisfies $\phi$.
+
+\paragraph*{LTS-Kripke Translation}
+A translation system $\eta$ maps states in LTSs to states in Kripke structures. This allows us to perform LTL/CTL validation on LTS: 
+\begin{equation*}
+    P \models_{\eta} \phi \iff \eta(P) \models \phi
+\end{equation*}
+
+\begin{definition}[De Nicola-Vaandrager Translation]
+    The \textbf{DV-translation} translates process graphs into Kripke structures. Let the process graph be defineed as $(S, I, \rightarrowtriangle)$, as was the case for LTS. 
+
+    The associated Kripke structure is $((S^{'}, I), \rightarrowtriangle^{'}, \models)$, where:
+    \begin{align*}
+        S^{'} \coloneqq& S \cup \{[s, a, t] \in \rightarrowtriangle | a \ne \tau\} \\
+        \rightarrowtriangle^{'} \coloneqq& 
+            \{(s, [s, a, t]), ([s, a, t], t) | [s, a, t] \in S^{'}\} \\
+            \cup& \{(s, t) | (s, \tau, t) \in \rightarrowtriangle \}
+    \end{align*}
+
+    In short, we create new states out of transitions due to visible actions, and create linkages accordingly. 
+\end{definition}
+
+\begin{theorem}
+    Processes $P, Q$ satisfy the same LTL formulas if: 
+    \begin{equation*}
+        P =_{CT}^{\infty} Q
+    \end{equation*}
+    Moreover, finitely-branching processes $P, Q$ satisfies \textbf{iff}.
+\end{theorem}
+
+\begin{theorem}
+    Processes $P, Q$ satisfy the same $LTL_{-X}$ formulas (i.e., LTL without $X$) if: 
+    \begin{equation*}
+        P =_{WCT}^{\infty} Q
+    \end{equation*}
+\end{theorem}
+
+\begin{theorem}
+    Processes $P, Q$ satisfy the same CTL formulas if: 
+    \begin{equation*}
+        P =_{B} Q
+    \end{equation*}
+    Moreover, finitely-branching processes satisfies \textbf{iff}. 
+
+    On the otherhand, when CTL is expanded to $CTL^{\infty}$ (i.e., CTL with infinite $\wedge$), all processes also satisfy \textbf{iff}. 
+\end{theorem}
+
+\begin{theorem}
+    A \textbf{divergence-free} process is one where no reachable state $p$ has $p \xrightarrow{\tau^\infty} !$ -- infinite $\tau$s. 
+    
+    Two \textbf{divergence-free} processes $P, Q$ satisfy the same ${CTL}_{-X}$ formulas if: 
+    \begin{equation*}
+        P =_{BB} Q
+    \end{equation*}
+
+    Moreover, when CTL is adjusted to ${CTL}^{\infty}_{-X}$, we have \textbf{iff}. Same goes if $P, Q$ are additionall finitely branching. 
+\end{theorem}
+
+\end{document}

09-concurrency.tex

@@ -0,0 +1,53 @@
+\documentclass[99-notes-packed.tex]{subfiles}
+
+\begin{document}
+\paragraph*{Concurrency Semantics} Define the following semantics of interest wrt. concurrency theory: 
+\begin{enumerate}
+    \item {
+        \textbf{Interleaving Semantics}: concurrent actions $a$, $b$ occur in one of the following orders: 
+        \begin{itemize}
+            \item $a; b$
+            \item $b; a$
+        \end{itemize}
+    }
+    \item {
+        \textbf{Step Semantics}: concurrent actions $a$, $b$ occur in one of the following orders: 
+        \begin{itemize}
+            \item $a; b$
+            \item $b; a$
+            \item $a || b$ (in parallel)
+        \end{itemize}
+    }
+    \item {
+        \textbf{Interval Semantics}: concurrent actions $a$, $b$ occur in continuous time, such that $a$, $b$ may occur in parallel for a subset of total runtime. 
+    }
+    \item {
+        \textbf{Partial-order (aka. Causal) Semantics}: concurrent actions $a$, $b$ not only can occur in parallel for some continuous time interval, but can also intersperse as unspecified segments (e.g., OS scheduling). 
+
+        Nevertheless, causal relationships between $a, b, \dots$ are preserved -- $a$ calling e.g. \texttt{fork()} will posit a partial ordering before the spawned task $b$, though the exact concurrency behaviors leave much leeway to the OS scheduler.
+    }
+\end{enumerate}
+
+\begin{definition}[Pomset]
+    A \textbf{pomset (partial-ordered multiset)} defines a $(E, <, l)$-tuple where:
+    \begin{itemize}
+        \item $E$ a set of ``events'' -- corresponding to each occurrence of action. 
+        \item $<$ a partial-order of E -- $e_i$ happens before $e_j$, or incomparable, etc.
+        \item $l: E \rightarrow A$ a mapping between events to their actions. 
+    \end{itemize}
+
+    A normal trace thus becomes a totally ordered multiset of actions, compared to a pomset representation. 
+\end{definition}
+
+\paragraph*{Petri Net} captures the dynamism within parallel systems. It defines a $(S, T, F, I)$-tuple where: 
+\begin{itemize}
+    \item $S, T$ define \underline{places} and actions grouped in bipartite form. 
+    \item $F \subseteq (S \times T) \cup (T \times S)$ set of transitions.
+    \item $I: S \rightarrow \mathbb{N}$ (initial marking) defines the initial state of control, via allocating tokens to initial states. Subsequent states of control is referred to as \textbf{marking} in general.
+\end{itemize}
+
+\begin{definition}[Control \& Tokens]
+    Petri nets encode control at runtime. A \textbf{control} simply refers to the state at which the system is currently at. It is symbolized by a \textbf{token} for each concurrent state. 
+\end{definition}
+
+\end{document}

99-notes-packed.tex

@@ -4,7 +4,6 @@
 \usepackage[T1]{fontenc}
 \usepackage[a4paper, margin=0.25cm, landscape]{geometry}
 
-
 \usepackage{multicol}                       % 2-col formatting
 \usepackage{hyperref}
 \usepackage[english]{babel}                 % theorem environ
@@ -17,6 +16,7 @@
 \usepackage{ebproof}
 \usepackage{amsmath}
 \usepackage{amssymb}
+\usepackage{cancel}
 
 \usepackage{subfiles}                       % multi-file project
 
@@ -24,6 +24,7 @@
 \newtheorem{definition}{Definition}[section]
 \newtheorem{background}{Background}[section]
 \newtheorem{example}{Example}[section]
+\newtheorem{theorem}{Theorem}[section]
 
 \begin{document}
 \begin{multicols*}{3}
@@ -40,5 +41,20 @@
 \section{Equational Axiomisation}
 \subfile{04-congruence.tex}
 
+\section{CSP; SOS}
+\subfile{05-csp.tex}
+
+\section{Hennessy-Miller Logic}
+\subfile{06-hml.tex}
+
+\section{Preorder and Simulation}
+\subfile{07-preorder.tex}
+
+\section{LTL; CTL; Kripke Structure}
+\subfile{08-ltl-ctl-kripke.tex}
+
+\section{Petri Net; Concurrency Semantics}
+\subfile{09-concurrency.tex}
+
 \end{multicols*}
 \end{document}