diff --git a/04-congruence.tex b/04-congruence.tex index 88a9391..0b5b098 100644 --- a/04-congruence.tex +++ b/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} \ No newline at end of file diff --git a/05-csp.tex b/05-csp.tex new file mode 100644 index 0000000..61a9a2a --- /dev/null +++ b/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} \ No newline at end of file diff --git a/06-hml.tex b/06-hml.tex new file mode 100644 index 0000000..2962c90 --- /dev/null +++ b/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} \ No newline at end of file diff --git a/07-preorder.tex b/07-preorder.tex new file mode 100644 index 0000000..2ab241e --- /dev/null +++ b/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} \ No newline at end of file diff --git a/08-ltl-ctl-kripke.tex b/08-ltl-ctl-kripke.tex new file mode 100644 index 0000000..aa43ddf --- /dev/null +++ b/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} \ No newline at end of file diff --git a/09-concurrency.tex b/09-concurrency.tex new file mode 100644 index 0000000..0e3388e --- /dev/null +++ b/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} \ No newline at end of file diff --git a/99-notes-packed.pdf b/99-notes-packed.pdf index c218890..cd3d941 100644 Binary files a/99-notes-packed.pdf and b/99-notes-packed.pdf differ diff --git a/99-notes-packed.tex b/99-notes-packed.tex index 31e3b9e..4b759cd 100644 --- a/99-notes-packed.tex +++ b/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} \ No newline at end of file