Logic - FLOLAC '17
===
###### tags: `flolac'17`, `Formal Verification`, `yenWu`, `kaizsv` , `張晏誠`, `郭燁廷`
# What is FLOLAC?
「邏輯、語言與計算」暑期研習營希望培養學員獨立進行基礎計算科學研究之能力，今年為第九屆。從第二年起，本研習營在兩大主題 — 程式語言(Programming Language)與正規驗證(Formal Verification)之間輪替。今年（奇數年）之主題為正規驗證，正式學分班課程名稱為「自動化正規驗證」。
本課程希望推廣程式驗證的重要性、知識與相關技能與學生，將講授與型式驗證領域之入門理論與知識，包含基礎邏輯(Logics)、計算理論(Theory of Computation)，以及各類常見的驗證主題，如字串程式(String-manipulating programs)驗證、時序邏輯(Temporal Logics)驗證、以自動機(Automata)為基礎之模型檢查(Model Checking)，並探討硬體合成(Hardware Synthesis)與軟體模型上的SMT驗證應用等等。希望透過一系列課程，培養學生以正規邏輯進行清晰思考的能力，了解邏輯與程式驗證的密切關係，以及計算理論與各類工具在驗證中扮演的角色，使學生能理解並解決程式驗證問題，能運用軟體工具輔助邏輯推理並證明程式之正確性，並具備在相關領域進行研究的能力。
自 2012 年起，本研習營正式成為台灣大學暑修課程，針對大學部學生開課，但亦歡迎研究生選修。 台灣大學學生可透過國立台灣大學暑期課程網選課，有學籍之其他學校學生可透過校際選修選課。無學籍之社會人士也可旁聽。
相關連結：
[FB粉絲頁連結](https://www.facebook.com/flolac.tw/)
[FLOLAC'17官方連結](http://flolac.iis.sinica.edu.tw/flolac17/doku.php)
# Outline
1. [Logic](#logic)
* [Propositional Logic](#propositional-logic)
* [Predicate Logic](#predicate-logic)
2. Computation
* [Elementary Computation Theory](#computation-theory)
3. [Satisfiability Modulo Theories(SMT)](#SMT)
* SMT - Introduce
* SMT - Decision Procedure
* SMT - Software Verification
4. Automata learning
* [Introduction](#an-introduction-to-automata-learning)
5. [Synthesis](#synthesis)
* [Boolean Satisfiability](#boolean-satisfiability)
6. [String](#string)
7. [Vienna Development Method](#vienna-development-method)
# Logic
先來考慮一個問題，$\land$是什麼？
很多人會回答是 and，沒錯，但他也有可能有任何意思，因為他本質上就是一個符號(symbol)而已，而後來我們給了他語義(semantic)，也就是賦予 syntax 特定 semantic，這點要特別注意，邏輯(logic)也就是規範 syntax來操作符號，並且我們有給定的公理(axiom)，是單純的符號操作，還沒有跟語意扯上關係。
:::info
補充
* [Difference Between Grammar, Syntax and Semantics](http://www.differencebetween.com/difference-between-grammar-and-vs-syntax-and-vs-semantics/)
:::
## Propositional Logic
顧名思義是個跟命題(proposition)有關係的邏輯，先來介紹什麼是命題
給個命題的例子
| | |
| - | - |
| p | 下雨 |
| q | 我有帶傘 |
| r | 我被淋濕 |
> 注意，這已經有給定語意了，但命題基本上只是能判斷對(true)或錯(false)的語句而已，我們確實能判斷有沒有下雨[name=Yen-Kuan Wu][color=#4d21b2]
我們可以使用邏輯而給出下面的型式
>$p \land \neg q \to r$
the conjuction of p and q imples r
附加上語意的型式都是
>If p and not q then r.
如果下雨且我沒帶傘，我就會被淋濕
現在開始我們開始站在 propositional logic上來說話
我們的語言是建構在 propositions(or declarative sentences)
什麼是 sentences? p, q, r, $p\land q$ 都是
特別注意我們說 p, q, r 是所謂的 atomic sentence，由於他無法在做拆解
我們可以透過以下的 connectives來建構新的 sentences:
* The **negation** of $p$ (denoted by $\neg p$)
* The **disjunction** of $p$ and $q$ (denoted by $p \lor q$)
* The **conjuction** of $p$ and $q$ (denoted by $p \land q$)
* The **implication** of $p$ and $q$ (denoted by $p \Rightarrow q$)
再來介紹如何從既有的 sentences 推斷(infer)新的 sentence
也就是所謂的 natural deduction，他包含了許多證明規則(proof rules)
一個 proof長怎樣呢？
$\phi_1,\phi_2,\phi_3,...,\phi_n\vdash\psi$
>我們稱整個是一個 sequent
>set of sentences $\phi_1,\phi_2,\phi_3,...,\phi_n$ (called **premises**)
>sentence $\psi$ (called **conclusion**)
這一串是一個有效的 (valid) 證明，在 $\vdash$ 之前的 $\phi_1, \phi_2,...,\phi_n$ 為前提 (permises)，$\psi$為從 permises 一步步推導出來的結論，如何推導接下來會介紹。
推導的規則有兩個 `introduction` 及 `elimination`，`introduction` 可以想成是從線索推導出想要證明的結論，`elimination` 則是將要證明的結論拆解成各別的線索，只要證明出各別的線索為真 (always True) 就可以證明出結論。
開頭的符號也可以寫成以下的形式，同樣代表在前提為真的情況下，可以推導出想要的結論$\psi$。
$$
{\phi_1, \phi_2,...,\phi_n\over\psi}
$$
我們說一個 sequent 是 valid 也就是可以找得到一個證明來證明他
這邊介紹 proof rules for natural deduction
>我們這邊只舉幾個例子其他更詳盡的教學和不同的 proof rules可以參考這邊
[Cornell 大學的教學網站](http://www.cs.cornell.edu/courses/cs3110/2013sp/lectures/lec15-logic-contd/lec15.html): natural deduction的簡介
[Wikipedia- propositial calculus](https://en.wikipedia.org/wiki/Propositional_calculus): 有詳盡的 prood rules以及 propositional logic的介紹
>[name=Yen-Kuan Wu][color=#4d21b2]
* Proof rules for conjunction
* Conjunction-introduction $\land i$
$$
{\phi\quad\psi\over\phi\land\psi}\land i
$$
> 由 $\phi$和$\psi$可以推到$\phi\land\psi$
> 從語意上來看就是，$\phi$和$\psi$都是 true的話，$\phi\land\psi$也會是 true
> 我們給這個 Conjunction-introduction 一個代號"$\land i$"
> [name=Yen-Kuan Wu][color=#4d21b2]
* conjunction-elimination $\land e$
$$
{\phi\land\psi\over\phi}\land e_1 \quad or \quad {\phi\land\psi\over\psi}\land e_2
$$
> 由$\phi\land\psi$可以推到 $\phi$或是 $\psi$
> 語意上就是，$\phi\land\psi$是true的話，$\phi$也會是 true
> 注意是"或"，所以他可以推到任何一個
> [name=Yen-Kuan Wu][color=#4d21b2]
:::info
來證明這個吧，$p \land q, r\vdash q \land r$
| | | |
| - | - | - |
| 1 | $p \land q$ | premise |
| 2 | r | premise |
| 3 | q | $\land e_2$ 1|
| 4 | $q \land r$ | $\land i$ 2, 3 |
其他的 rule也是同樣的操作方法
:::
再來我們思考如何讓電腦幫我們呢？ 先從這幾個問題下手
在我們看來 $p\land q$和 $q\land p$根本是一樣的東西，但電腦分不出來$p\land q\Rightarrow r\Rightarrow w$，我們其實很清楚順序，但電腦不知道，這些都是需要我們要跟電腦說的。
> $\neg$ -> {$\lor, \land$} -> $\Rightarrow$
所以我們能知道順序了
這個是什麼 $pp\land\land qq$，怪怪的對吧，這你也要跟電腦講
* 在 propsitional logic 之上，我們的 well-formed formula(WFF) 是按照以下規則，並且是有限次的
* atom: 每個 propositional atom p, q, r ... 都是 WFF
* $\neg$: 如果 $\phi$是 WFF，那$(\neg\phi)$也是 WFF
* $\land$: 如果 $\phi$ 和 $\psi$是 WFF，那$(\phi\land\psi)$也是 WFF
* $\lor$: 如果 $\phi$ 和 $\psi$是 WFF，那$(\phi\lor\psi)$也是 WFF
* $\Rightarrow$: 如果 $\phi$ 和 $\psi$是 WFF，那$(\phi\Rightarrow\psi)$也是 WFF
> [Wikipedia - well-formed formula](https://en.wikipedia.org/wiki/Well-formed_formula)[name=Yen-Kuan Wu][color=#4d21b2]
$(((p \land q) \Rightarrow r) \Rightarrow w)$ 有效
$((pp) (\land\land (qq)))$ 無效
所以我們可以分辨有效的 formula了
:::info
補充
* [命題](https://zh.wikipedia.org/wiki/%E5%91%BD%E9%A2%98)
* [命題邏輯](https://zh.wikipedia.org/wiki/%E5%91%BD%E9%A2%98%E9%80%BB%E8%BE%91)
:::
## Predicate Logic
簡單來講 Predicate Logic 就是填空。先考慮一個例子，「``每位學生都比某位授課者年輕。``」，我們無法用前述的 Propositional Logic 精確地描述該句子。
:::warning
想想看
* s: 每位學生
* t: 某位授課者
* y: 年輕 (誰比誰年輕?)
:::
因此可以填空的方式來描述，再引入兩個符號 $\forall$ 代表「所有」，$\exists$ 代表「存在」。
:::info
* S(x): x 是學生
* T(x): x 是授課者
* Y(x, y): x 比 y 年輕
上述的例子可以表示成 $\forall x(S(x) \Longrightarrow (\exists y(T(y)\land Y(x, y))))$
:::
### Syntax of Predicate Logic
* $\mathcal{P}$: **predicate symbols**，像是上面的 S(x)，會挖一個空格，填入 x，例如 S(Andy) 意思是「Andy 是學生」。其結果是 True 或 False。
* $\mathcal{F}$: **function symbols**，例如 m(Andy)，可以解釋為「Andy 的媽媽是」，結果會傳回一個 Term Amy，整體的意思是「Andy 的媽媽是 Amy」。
* $\mathcal{C}$: **constant symbols**，只是一個項目，例如 Amy, Andy。
* 若 $f \in\mathcal{F}$，其 $f$ 有 n 個參數，則稱其為 n-arity function。
* **Terms** 的定義為 $t ::= \mathcal{C} | \mathcal{F}$，只要是 constant symbols 或是 function 回傳的都叫 Terms。
* **Formulae** 則定義為 $\phi::=\mathcal{P}|(\lnot\phi)|(\phi\land\phi)|(\phi\lor\phi)|(\phi\Longrightarrow\phi)|(\forall x\phi)|(\exists x\phi)$，對所有在 $\mathcal{P}$ 內的 predicate symbols 進行以上的操作都可以稱為 Formulae。
:::info
Example: "every son of my father is my brother"
* S(x, y): x is a son of y
* F(x, y): x is the father of y
* B(x, y): x is a brother of y
$$
\forall x\forall y(F(x, me)\land S(y, x)\Longrightarrow B(y, me))
$$
* f(x): father of x
$$
\forall x(S(x, f(me))\Longrightarrow B(x, me))
$$
:::
* **Free and Bound variables**: 考慮一個 formulae，若 leaf node 沒有被 $\forall x$ 或是 $\exists x$ 控制，則稱它為 free variables，反之稱為 bound variables。
```graphviz
digraph {
node [shape=circle]
⇒->{∀x ⋁}; ∀x->{∧};
∧->{{P1[label=P]} {Q1[label=Q]}};
P1->{x1[label=x]};
⋁->{⌐ {Q2[label=Q]}};
Q1->{x2[label=x]}; Q2->y;
⌐->{P2[label=P]}
P2->{x3[label=x]}
}
```
$(\forall x(P(x)\land Q(x)))\Longrightarrow(\lnot P(x)\lor Q(y))$
* **subsitution**: 在 formula $\phi$ 內的 free variable x，可以用 $\phi [t/x]$ 表示將 $\phi$ 內的 free variable x 用 t 替換。
```graphviz
digraph {
node [shape=circle]
⇒->{∀x ⋁}; ∀x->{∧};
∧->{{P1[label=P]} {Q1[label=Q]}};
P1->{x1[label=x]};
⋁->{⌐ {Q2[label=Q]}};
Q1->{x2[label=x]}; Q2->y;
⌐->{P2[label=P]}
P2->{f}
f->{x3[label=x] y1[label=y]}
}
```
$(\forall x(P(x)\land Q(x)))\Longrightarrow(\lnot P(x)\lor Q(y))[f(x, y)/x]$
### Proof theory of Predicate Logic
* **Universal Quantification**
$$
{\forall x\phi\over\phi[t/x]}\forall xe \quad\quad {\boxed{x_0 \\\quad.\\\quad.\\\quad.\\\quad\phi[x_0/x]}\over\forall x\phi}\forall xi
$$
對 $\forall xe$ 而言就是找一個 term t 代入 x，但 t 有限制，前面提到 $\phi[t/x]$ 中的 x 必須為 $\phi$ 的 free variable，而 t 不能有 $\phi$ 的 bound variable，若要強制替換必須要換變數名稱，參考[lambda calcus](https://en.wikipedia.org/wiki/Lambda_calculus#.CE.B1-conversion)；而 $\forall xi$ 是先假設有一個 $x_0$ 滿足 $\phi[x_0/x]$ 則可以推導出 $\forall x\phi$。
* **Existential Quantification**
$$
{\phi[t/x]\over \exists x\phi}\exists xi \quad \quad{\exists x_0\quad\boxed{x_0\\\quad\phi[x_0/x]\\\quad.\\\quad.\\\quad.\\\quad\mathcal{X}}\over\mathcal{X}}\exists xe
$$
$\exists xi$ 的條件與 $\forall xe$ 類似。而 $\exists xe$ 則是說，要從 $\exists x\phi$ 證明 $\mathcal{X}$，先假設一個 variable $x_0$ 使得從 $\phi[x_0/x]$ 可以得到結論 $\mathcal{X}$，如此可證明 $\mathcal{X}$。
:::success
More Examples: [Logic and Proof](http://www.phil.cmu.edu/projects/logicandproofs/alpha/htmltest/m12_pred_derivations/translated_chapter12.html)
:::
### Semantics of Predicate Logic
Let $\mathcal{M}$ be the model of Predicate Logic, then it consists of $(\mathcal{F}, \mathcal{P})$.
Let $\mathcal{F} = \{e,.\}$ and $\mathcal{P} = \{\le\}$ where $e$ is a constant for empty string, $.$ a binary function for concatenation, and $\le$ a binary predicate for less than or equal to.
There is also an Environment $I: var \rightarrow A$ mapping a variable to values.
$$
I[X\mapsto a](y) = \begin{cases}a & \text{if x = y}\\ I(y) & \text{if x} \neq \text{y}\end{cases}
$$
先定義些名詞，$\Gamma$ 是一個包含 predicate logic formula 的集合 (有可能是無限集合)，$\psi$ 是 predicate logic formula 也就是結論。
* **holds**: $\Gamma\vDash\psi$ holds，對每個 model $\mathcal{M}$ 及 environment $I$，若
$$
\text{if for every }\phi\in\Gamma, \mathcal{M}\vDash_I \phi\text{ holds, then } \mathcal{M}\vDash_I \psi\text{ holds.}
$$
* **satisfiable**: 若存在一個 model $\mathcal{M}$ 及 environment $I$，使得 $\mathcal{M}\vDash_I \psi$ holds。
* **valid**: 對每個 model $\mathcal{M}$ 及 environment $I$，$\mathcal{M}\vDash_I \psi$ holds。
# Computation Theory
這邊演算法課程也會提到, 可能有人覺得理論
可是這是有實際使用的例子, 並且還有人利用這技術成功獲利(就是下面String的驗證)
[課程](http://flolac.iis.sinica.edu.tw/flolac17/doku.php?id=course:computation)
輔助學習的工具: [GOAL: Graphical Tool for Omega-Automata and Logics](http://goal.im.ntu.edu.tw/wiki/doku.php#download)
## $\mathbf {Finite\space state\space automata}$
### $\mathbf {Finite\space State\space Automata}$
A finite state automation is a 5-tuple$(Q,\Sigma,\delta,I,F)$
where
* $Q\space is\space a\space finite\space set\space of\space \color{red} {states}$
* $\Sigma\space is\space a\space finite\space \color{red} {alphabet}$
* $\delta:Q\space\times\space\Sigma\to2^Q\space is\space the\space \color{red} {transition\space function}\\(somtimes\space written\space as\space a\space relation\space \delta:\space Q\space\times\Sigma\space\times\space Q)$
* $I\subseteq Q\space is\space the\space set\space of\space \color{red} {initial\space states}$
* $F\subseteq Q\space is\space the\space set\space of\space \color{red} {accepting(final)states}$
#### $\mathbf {alphabet}$
* $An\space alphabet\space is\space a\space symbols.$
* $Symbol\space can\space be\space \color{red} {classical}\space and\space \color{red} {propositional}$
##### alphabet example
#### $\mathbf {\epsilon-Transitions}$
* $Assume\space \epsilon\notin\Sigma(alphabet)$
* $An\space \epsilon-transitions\space is\space a\space transition\space that\space does\space not\space need\space to\space consume\space any\space symbol.$
* $\epsilon-transitions\space are\space only\space allowed\space in\space NFA.$
* $DFA\space and\space NFA\space with\space \epsilon-transitions\space have\space the\space same\space expressive\space power.$
##### $\mathbf {Elimination\space of\space \epsilon-Transitions}$
#### Automata example
#### $\mathbf {Deterministic\space Finite\space Automata(DFA)}$
* $An\space automaton\space M=(Q,\Sigma,\delta,I,F)\space is\space \color{red} {deterministic}\space if$
* $\vert I\vert=1,and$
* $\vert \delta(s,a)\vert=1\space for\space all\space s\in Q\space and\space a\in \Sigma$
##### $\mathbf {How\space to\space get\space a\space DFA\space from\space an\space automata}$
##### $\mathbf{Closure\space Properties}$
###### $\mathbf{Union}$
* $M_1 = (Q_1, Σ,\delta_1, I_1, F_1),\space M_2 = (Q_2, Σ, \delta_2, I_2, F_2)$
* $Assume\space Q_1 \cap Q_2 = \emptyset$
* $M3 = (Q_1 \cup Q_2, Σ, \delta_3, I_1 \cup I_2, F_1 \cup F_2) where (s, a, t) \in\delta_3\space if$
* $(s, a, t) \in \delta_1, or$
* $(s, a, t) \in \delta_2$
* $L(M_3) = L(M_1) \cup L(M_2)$
###### $\mathbf{Intersection}$
* $M_1 = (Q_1, Σ, \delta_1, I_1, F_1),\space M_2 = (Q_2, Σ, \delta_2, I_2, F_2)$
* $M3 = (Q_1 × Q_2, Σ, \delta_3, I_1 × I_2, F_1 × F_2)\space where ((s_1, s_2), a, (t_1,t_2)) \in \delta_3\space if$
* $(s_1, a, t_1) ∈ \delta_1, and$
* $(s_2, a, t_2) ∈ \delta_2$
* $L(M_3) = L(M_1) \cap L(M_2)$
###### $\mathbf{Concatenation}$
* $M_1 = (Q_1, Σ, \delta_1, I_1, F_1),\space M_2 = (Q_2, Σ, \delta_2, I_2, F_2)$
* $Assume\space Q_1 \cap Q_2 = \emptyset\space and\space \epsilon\notin Σ.$
* $M_3 = (Q_1 \cup Q_2, Σ \cup \{\epsilon\}, \delta_3, I_1, F_2) where (s, a, t) ∈ delta_3\space if$
* $(s, a, t) \in \delta_1,$
* $(s, a, t) \in \delta_2, or$
* $a = \epsilon, s \in F_1, and\space t \in I_2.$
* $L(M_3) = L(M_1)L(M_2) = \{ uv | u \in L(M_1)\space and\space v \in L(M_2) \}$
###### $\mathbf{Kleene\space Closure}$
* $M = (Q, Σ, \delta, I, F)$
* $Assume\space \epsilon \notin Σ\space and\space s_s \notin Q.$
* $M’ = (Q \cup \{s_s\}, Σ \cup \{\epsilon\}, \Delta, \{s_s\}, F \cup \{s_s\}) where (s, a, t) \in \Delta\space if$
* $s = s_s,\space t \in I,\space and\space a = \epsilon,$
* $(s, a, t) \in \delta,\space or$
* $s \in F, t \in I,\space and\space a = \epsilon.$
* $L(M’) = L(M)^*$
###### $\mathbf{Complementation\space DFA}$
* $M = (Q, Σ, \delta, I, F)\space is\space a\space DFA.$
* $M’ = (Q, Σ, \delta, I, Q \setminus F)$
* $L(M’) = Σ^* \setminus L(M)$
###### Closure Properties example
##### $\mathbf{Minimization}$
* Minimal DFA's or NFA's the number of states.
* Given a DFA M1,we can construct a minimal DFA M2 such that L(M1) = L(M2)
* Given an NFA M1,we can construct a minimal NFA M2 such that L(M1) = L(M2)
###### $\mathbf{Myhill-Nerode\space Theorem}$
* $Given\space a\space language\space L \subseteq Σ^*,\space define\space a\space binary\space relation\space R_L\space over\space Σ^*\space as\space follows.$
* $xR_Ly\space iff\space \forall z \inΣ^*\space (xz \in L\leftrightarrow yz \in L)$
* $R_L\space can\space be\space shown\space to\space be\space an\space equivalence\space relation.$
* $R_L\space divide\space the\space set\space of\space string\space into\space \color{red}{equivalence\space classes}.$
* $L\space is\space regular\space iff\space R_L\space has\space a\space finite\space number\space of\space equivalence\space classes.$
* $The\space number\space of\space states\space in\space the\space minimal\space DFA\space \\recognizing\space L\space is\space equal\space to\space the\space number\space of\space equivalence\space classes\space in\space R_L.$
###### $\mathbf{Equivalence\space Classes}$
* The relation R is an equivalence relation if it is
* $reflexive:\space \forall s \in S.\space sRs;$
* $symmetric:\space \forall s_1,s_2 \in S.\space s_1Rs_2 \rightarrow s_2Rs_1;$
* $transitive:\space \forall s_1,s_2,s_3 \in S.\space s_1Rs_2 \land s_2Rs_3 \rightarrow s_1Rs_3$
* $The\space \color{red}{equivalence\space class}\space of\space s\in S\space under\space R\space is\space the\space set\space [s]_R\stackrel{\text{def}}{=}{s^{'}\in S:sRs^{'}}$
###### $\mathbf{Minimization\space Idea}$
* For a language L ⊆ Σ*, compute the equivalence classes of L.
* Construct a state for each equivalence class.
* $A\space equivalence\space class\space C_1\space can\space take\space an\space a-transition\space to\space another\space equivalence\space class\space C_2\space \\if\space there\space is\space a\space string\space x \in C_1 such\space that\space x_a \in C_2.$
###### $\mathbf{How\space to\space find\space the\space equivalence\space classes?}$
* [Hopcroft’s Algorithm](https://en.wikipedia.org/wiki/DFA_minimization#Hopcroft.27s_algorithm)
### $\mathbf {Finite\space State\space Automata\space Semantics}$
* $Let\space M = (Q,\Sigma,\delta,I,F)\space be\space a\space finite\space state\space automaton$
* $Let\space w=a_0a_1a_2\cdots a_{n-1}\space be\space a\space \color{red} {word}\space over\space \Sigma$
* $A\space \color{red}{run}\space of\space w\space on\space M\space is\space a\space sequence\space of\space states\space s_0s_1s_2\cdots s_{n-1}where$
* $s_0\in I$
* $(s_i,a_i,s_{i+1})\in\delta$
* The empty word is denoted by $\color{red}{\epsilon}$.
* $A\space run\space s_0s_1s_2\cdots s_{n}\space is\space \color{red}{accepting}\space if\space s_n\in F$
* $A\space word\space w\space is\space \color{red}{accepted}\space by\space M\space if\space there\space is\space an \space accepting\space run\space of\space w\space on\space M$
* $The\space \color{red}{language}\space of\space M\space is\space the\space set\space of\space word\space accepted\space by\space M,denoted\space by\space \color{red}{L(M)}$
* $The\space language\space recognized\space by\space a\space finite\space state\space automaton\space is\space a\space \color{red}{regular\space language}.$
* $An\space automaton\space M\space is\space \color{red}{empty}\space if\space L(M)=\emptyset$
* $An\space automaton\space M\space is\space \color{red}{universal}\space if\space L(M)=\Sigma^*$
* $Two\space automata\space are\space \color{red}{equivalent}\space if\space they\space recognize\space the\space same\space language.$
講了一堆定義 , 還是來看個例子吧
#### Finite state automata example
$\Sigma$是alphabet , 這邊已經寫出來
automata以$(Q,\Sigma$,$\delta,I,F)$表示
說明每個符號是什麼
* $Q$就是state的集合 , 圖中圈圈（雙層圈圈也算）內的符號 , 所以是$Q=\{s_0,s_1\}$
* $Sigma$是輸入符號的集合 , 這邊每個state到另一個state的有箭頭的線是transition , 線下的符號就是此automate從某個state到另一個state的input , $\Sigma=\{a,b\}$
* $\delta$就是transition function , 用$(s_0,a,s_1)$來代表圖上一個有箭頭的線 , $s_0$是線的起點 , $a$是圖上線的輸入, $s_1$就是箭頭所指的state , 以這張圖為例 , $\delta=\{(s_0,b,s_0),(s_0,a,s_1),(s_1,a,s_1),(s_1,b,s_0)\}$
* $I$就是initial states , 也是個集合 , 以這張圖 , 就是左邊那條有箭頭的線指到的$s_0$ , initial states可以有多個 , $I=\{s_0\}$
* $F$就是accepting (final) states , 也是個集合 , 就是圖中雙層圈圈 , 可以有多個 , $F=\{s_1\}$
接下來說明Semantics的部份
先舉個$word$的$run$好了
選$word=aabb$ , 代表從initial states依序輸入aabb
一般來說 , state的轉移可能有多個(有相同的輸入指到不同的state)
從上圖舉一個例子:
$aabb$對應的$run$是$s_0s_1s_1s_0s_0$
然後$run$最後的state , 如果是$F$(accepting (final) states)內的state , 那該$word$就是$L(M)$(language)內的元素
以$aabb$的$run$來講 , 最後是$s_0$ , 這不是F內的state , 所以$aabb\notin L(M)$
## $Regular\space Expressions$
### Definition
* Let Σ be an alphabet.
* The regular expressions over Σ are defined as follows.
* $\color{red}{\emptyset}\space is\space a\space \color{blue}{regular\space expression}\space denoting\space the\space empty\space set;$
* $\color{red}{\epsilon}\space is\space a\space \color{blue}{regular\space expression}\space denoting\space the\space set\space \color{red}{\{\epsilon\}};$
* $for\space each\space \color{red}{a} \in \Sigma,\space \color{red}{a}\space is\space a\space \color{blue}{regular\space expression}\space denoting\space the\space set\space \color{red}{\{a\}};$
* $if\space \color{red}{r}\space and\space \color{red}{s}\space are\space \color{blue}{regular\space expressions}\space denoting\space the\space sets\space \color{red}{R}\space and\space \color{red}{S}\space respectively,\space \\then\space \color{red}{r+s},\space \color{red}{rs},\space and\space \color{red}{r^*}\space are\space \color{blue}{regular\space expressions}\space \\denoting\space \color{red}{R∪S}, \color{red}{RS},\space and\space \color{red}{R^*}\space respectively.$
* $The\space language\space of\space a\space regular\space expression\space e\space is\space denoted\space by\space L(e).$
### Regular Expressions Examples
讓$\Sigma=\{a,b\}$
$a^*ba^* = \{w | w\space has\space exactly\space a\space single\space b\}$
$a^*ba^*$內可以有$aba$或$ba$
:::info
$a^*$
星號指的是克萊尼星號
代表可選的$word$可以是空字串($\epsilon$),a,aa,a...有n個
[wiki連結](https://zh.wikipedia.org/wiki/%E5%85%8B%E8%8E%B1%E5%B0%BC%E6%98%9F%E5%8F%B7)
:::
再多幾個例子
$r+\emptyset=r$
$r+\epsilon=r+\epsilon$
$r\emptyset=\emptyset$
$r\epsilon=r$
### Regular Expressions VS Finite State Automata
* A language is recognized by an NFA if and only if some regular expression describes it.
* A language is regular if and only if some regular expression describes it.
* Let $$A_r$$ be an NFA recognizing the language of a regular expression r.
* $r+s:\space union\space of\space A_r\space and\space A_s$
* $rs:\space concatenation\space of\space A_r\space and\space A_s$
* $r^*:\space the\space Kleene\space closure\space of\space A_r$
#### From NFA to RE
* Transitive Closure Method
* State Removal Method
* Brzozowski Algebraic Method
##### Transitive Closure Method
* $Let\space D = (\{s_1, …, s_n\}, \Sigma,\delta , \{s_1\}, F)\space be\space a\space DFA.$
* Define
* $R_{ij}^0= {a | (s_i, a, s_j) \in \delta}\space if\space i \neq j$
* $R_{ij}^0= \{a | (s_i, a, s_j) \in \delta\} \cup \{\epsilon\}\space if\space i = j$
* $R_{ij}^k= R_{ik}^{k-1}(R_{kk}^{k-1})^*R_{kj}^{k-1}\cup R_{ij}^{k-1}$
* $R_{ij}^k\space represents\space the\space inputs\space that\space cause\space D\space to\space go\space from\space s_i\space to\space s_j\space \\without\space passing\space through\space a\space state\space higher\space than\space s_k.$
* $R_{ij}^k\space can\space be\space denoted\space by\space regular\space expressions.$
* $L(D) = \bigcup_{S_j \in F} R_{1j}^n$
##### State Removal Method
##### Brzozowski Algebraic Method
#### An Example From NFA to RE
## $WS1S$
* Syntax of S1S(monadic second-order logic of one sucessor)
* First-order variable set: V = {$x_1,x_2,...$}
* Second-order variable set: X={$X_1,X_2,...$}
* Terms t::0|$x_i
* Formula $\phi ::= S(t,t)|X_i(t)|\neg\phi |\phi\land\phi|\exists x.\phi|\exists X.\phi$
* S is the successor predicate.(EX.S(1,2)=True) , X(t) means t $\in$ X
* WS1S:fragment of S1S which allows only quantification over finit sets
* WS1S on Words
* Let \Sigma be a finite set of alphbet.
* A word is defined as w=$a_0a_1...a_n$
* A unary predicate $P_a$ is defined for every a$\in\Sigma$ such that $P_a(i)$ if and only if $a_i=a$
* Buchi Theorem : a language L$\subseteq\Sigma^*$ is regular if and only if L is expressible in WS1S
* WS1S Examples
* The last symbol is a
* $\exists x.\\(P_a(x)\land -\exists y.(x<y))$
* contains substring ab
* $\exists x.\exists y.(P_a(x)\land P_b(y)\land S(x,y))$
* has substring b$a^*$b
* $\exists x.\exists y.(x<y \land P_b(x)\land P_b(y)\land \forall z((x<z\land z<y)\to P_a(z)))$
## $\omega-Automata$
一般的自動機，是以有限的字母組成。但現實上，我們考量的系統常常是不會停止的，如果我們想把自動機運用在這類的系統上的話，我們必須建立擁有無限字母的自動機。而$\omega-Automata$就是一種實現方式。
### 定義
An $\omega-Automata$ is a tuple (Q,$\Sigma ,\delta ,q_0$,Acc)where
* Q is a finite set of states
* $\Sigma$ is a finte alphbet
* $\delta : Q \times\Sigma\to 2^Q$ is the transition function
* $q_0$ is the initial state,
* Acc is the acceptance condition
### 語意
Let M be an $\omega-Automata$,if $\omega = a_0a_1$...be an infinite word over $\Sigma$.
Then a run of $\omega$ is a sequence of state $q_0q_1...$ where $(q_i,a_i,q_{i+1})\in\delta$
## $Linear\space Temporal\space Logic$
### Linear Model Checking
* LTL為一種時序邏輯，可用於檢驗線性時間的狀況(EX.排程上的可行性)
* 檢查方式:檢查我們的modle 是否包含在規約裡面；以較數學的寫法:L(M)$\bigcap L(A_{-f})$ 是否為空集合
### LTL 語意
* $(\rho,i)\models p$ iff p$\in s_i$
* $(\rho,i)\models -f$ iff p$(\rho,i)\nvDash f$
* $(\rho,i)\models f\land g$ iff $(\rho,i)\models f$ and $(\rho,i)\models g$
* $(\rho,i)\models Xf$ iff $(\rho,i+1)\models f$
* $(\rho,i)\models Ff$ iff $(\rho,i)\models f$ for some j$\geqq$ i
* $(\rho,i)\models Gf$ iff $(\rho,i)\models f$ for all j$\geqq$ i
* $(\rho,i)\models fUg$ iff exists j$\geqq$ i such that $(\rho,i)\models g$ and for all i $\geqq$k<j $(\rho,k)\models f$
* $(\rho,i)\models fUg$ iff exists j$\geqq$ i such that $(\rho,i)\models f$ and for all i $\geqq$k<j,$(\rho,i)\models g$ or for all j$\geqq$i,$(\rho,i)\models g$
### LTL 小整理
* $\rho\models f$: a state sequence $\rho$ satisfies an LTL formula f
* $\rho\models f$ iff $(\rho,0)\models f$
* $\models f$: an LTL formula f is valid
* $\models f$ iff $\rho\models f$ for all $\rho$
* fRg = -(-fU-g)
* Fg = true U g
* Gf = false R f
* infinitely often:GF
* -Fg = G -g
* -Gf = F -f
# Software Verification
# ==Satisfiability Modulo Theories==
## Introduction
* Model checking
* Craig interpolation
* **Satisfiability modulo theories**
# SMT
> [Slides from flolac 17](http://flolac.iis.sinica.edu.tw/flolac17/lib/exe/fetch.php?media=course:01_smt.pdf)
> Ref: [Wikipedia- List of logic symbols](https://en.wikipedia.org/wiki/List_of_logic_symbols)
### Recall First-Order Logic
First-Order Logic abbreviation "FOL"
* Term
* Variables: $x, y ,...$
* Function symbols: $f, g, ...$
* Fomulas
* Preducate symbols: $p, q, ...$
* Logic symbols: $\neg, \wedge, \land, \rightarrow, \leftrightarrow$
* **==Quantifications==**: $\forall, \exists$
* A **FOL formula** is interpreted under a model and an environment
* Model: **gives the meanings** of funciton symbols and predicate symbols
* Environment: **gives the value** of variables
* Signature: a collection of non-logical symbols excluding variables
## First-Order Theory
* A first-order theory $T$ is defined by:
* Signature $\Sigma$
* Axioms $A$: set of ==closed== ==$\Sigma$-formula==
> ==closed==: no free variables
> ==$\Sigma$-formula==: a FOL foumula constructed from the signature $\Sigma$ plus variables, logical connectives, and quantifiers.
:::info
Signature 是一個不包含 variables 及 邏輯符號的符號集合
(0, S, +, =)
($\varnothing$, $\subseteq$)
Axions 是一由 Signature 符號而來的 closed formula set
:::
* A ==$T$-model==: a model that ==satisfies the axioms== of first order theory $T$
* A ==$\Sigma$-formula $\varphi$== is ==valid== in the theory $T$, or $T$-valid, if every $T$-model M satisfies $\varphi$
* $T\vDash\varphi$ if $\varphi$ is ==valid==
* A $\Sigma$-formula $\varphi$ is ==satisfiable== in $T$, or $T$-satisfiable, if there is a $T$-model $M$ that statisfies $\varphi$
* A theory $T$ is ==complete== if for every closed $\Sigma$-formula $\varphi$, $T\vDash\varphi$ or $T\vDash\neg\varphi$
* A theory is ==consistent== if there is at least one $T$-model
* Two formulas $\varphi$ and $\psi$ are ==equivalent== in $T$, or $T$-equivalent, if $T\vDash\varphi\leftrightarrow\psi$
## Decidability
* Equality
* Peano arithmetic
* Presburger arithmetic
* Linear integers
* Recursive data structures
* Arrays
:::info
在繼續之前先來看幾個會用到的 Relation
* Binary Relation: $\text{for 2 elements }s_1,s_2\in S\text{, either } s_1 R s_2\text{ or }\lnot(s_1 R s_2)$
* Equivalence Relation:
* reflexive: $\forall s\in S.sRs$
* symmetric: $\forall s_1,s_2\in S.s_1 R s_2\rightarrow s_2 R s_1$
* transitive: $\forall s_1, s_2, s_3\in S. s_1 R s_2\land s_2 R s_3\rightarrow s_1 R s_3$
* Congruence Relation: $\forall S,T.(\land_{i=1..n}s_i R t_i)\rightarrow f(S)Rf(T)$
:::
### Equality $T_E$
* $\Sigma_E :\{=,a,b,c...p,q,r...\}$
* =, binary predicate
* Axioms of $T_E$
* Reflexivity: $\forall x. x=x$
* Symmetry: $\forall x,y. x=y\rightarrow y=x$
* Transitivity: $\forall x,y,z. x=y \rightarrow y=z\rightarrow x=z$
* Function congruence: $\text{for n-ary (n>0) functional symbol }f,\\\forall x_1..x_n,y_1..y_n.(\land_{i=1..n}.x_i=y_i)\rightarrow f(x_1..x_n) = f(y_1..y_n)$
* Predicate congruence: for n-ary predicate symbol $f$, $\forall x_1..x_n y_1..y_n.(\land_{i=1..n}x_i=y_i)\rightarrow(p(x_1..x_n)\leftrightarrow p(y_1..y_n))$
* $T_E$-valid is undecidable. The formula $F$ is always True if $F$ is $T_E$-valid; however, if $F$ is $T_E$-invalid, it can not always say False.
### Peano Arithmetic $T_{PA}$
* $\Sigma_{PA}:\{0, 1, +, ., =\}$
* $0$ and $1$ are constants.
* $+$, $.$ are binary functions
* $=$ is binary predicate
* Axioms of $T_{PA}$
* zero: $\forall x.\lnot(x+1=0)$
* Successor: $\forall x.y.x+1=y+1\rightarrow x=y$
* Induction: $P[0]\land (\forall x.P[x]\rightarrow P[x+1])\rightarrow\forall x.P[x]$
* Plus zero: $\forall x.x+0=x$
* Plus Successor: $\forall x.y.x+(y+1)=(x+y)+1$
* Times Zero: $\forall x.x*0=0$
* Times Successor: $\forall x.y. x*(y+1)=x*y+x$
* Intended Models of $T_{PA}$
* $\alpha_M[0]\text{ maps symbols `0` to }0_\mathbb{N}\in\mathbb{N}$
* same as $\alpha_M[1]$
* $\alpha_M[+]$: addition over $\mathbb{N}$
* $\alpha_M[.]$: multiplication over $\mathbb{N}$
* $\alpha_M[=]$: equality over $\mathbb{N}$
* Gödel showed that for every **recursive formula** $f:\mathbb{N}^n\rightarrow\mathbb{N}$ there is a $\Sigma_{PA}$ $F[x_1..x_n,r]$ that $F[x_1..x_n]\leftrightarrow r=f(x_1..x_n)$ (Gödel's first incompleteness theorem)
* Not allow multiplication
### Presburger Arithmetic $T_{\mathbb{N}}$
* $\Sigma_{PA}:\{0, 1, +, =\}$
* Axioms of $T_{PA}$
* zero: $\forall x.\lnot(x+1=0)$
* Successor: $\forall x.y.x+1=y+1\rightarrow x=y$
* Induction: $P[0]\land (\forall x.P[x]\rightarrow P[x+1])\rightarrow\forall x.P[x]$
* Plus zero: $\forall x.x+0=x$
* Plus Successor: $\forall x.y.x+(y+1)=(x+y)+1$
* Intended Model is same sa Peano Arithmetic
* Presburger showed that $T_{\mathbb{N}}$ is decidable.
* Validity of $\Sigma_{\mathbb{N}}$ formulas can be decided by procedures for the validity of $\Sigma_{\mathbb{Z}}$ formulas.
:::warning
For more theories and examples. Please check the [slides of FLOLAC](http://flolac.iis.sinica.edu.tw/flolac17/lib/exe/fetch.php?media=course:01_smt.pdf) and [an additional material](https://people.mpi-sws.org/~piskac/teaching/decpro-ws12/slides/theories.pdf).
| Theory | Description | Full | QFF () |
| -------- | -------- | -------- | ------ |
| $T_E$ | equality | no | yes |
|$T_{PA}$|Peano arithmetic|no|yes|
|$T_{\mathbb{N}}$|Presburger arithmetic|yes|no|
|$T_{\mathbb{Z}}$|linear integers|yes|yes|
|$T_{\mathbb{R}}$|reals (with * )|yes|yes|
|$T_A$|arrays|no|yes|
ps QFF: quantifier-free fragment
:::
:::danger
Combinatin Theories and Nelson-Oppen Approach
:::
# SMT - Decision Procedures
### Theory of Equality
* $\Sigma_E: \{=, a,b,c,..,f,g,h,..,p,q,r..\}$
* $\Sigma_E$-$formulae$
* $x=g(y,x)\rightarrow f(x)=f(g(y,z))$
* $f(f(f(a)))=a\land f(f(f(f(f(a)))))=a\land f(a)\neq a$
### Function Congruence
$\forall X,Y.(\land_{i=1..n}x_i=y_i\rightarrow f(X)=f(Y))$
### Predicate Congruence
$\forall X,Y.(\land_{n=1..n}x_i=y_i\rightarrow (p(X)\leftrightarrow p(Y)))$
## Congruence Closure Algorithm
:::info
Example: if following $\Sigma_E$-formula $T_E$-satisfiable?
$$
f(f(f(a)))=a\land f(f(f(f(f(a)))))=a\land f(a)\neq a
$$
1. $f(f(f(f(a)))) = f(a)$
(function congruence)
2. $f(f(f(f(f(a))))) = f(f(a))$
(function congruence)
3. $f(f(a)) = f(f(f(f(f(a)))))$
(symmetry)
4. $f(f(a)) = a$
(transitivity)
:::
請看上面的例子，當對 $\Sigma_E$ formula 使用 Equality Axioms (`symmetry`, `reflexivity`, `transitivity`, `congruence`) 產生的等式會比原本 $F$ 的 terms 還多 （$s = t$ or $s\neq t$），但考慮到 $F$ 內的 terms 是有限個，所產生的等式應該也要有限個，這樣繼續做下去可能會有 2 種情況
1. 一直 apply `symmetry` 及 `transitivity` 產生無限個等式
2. 產生的結果與 formula 不符 ($s\neq t$)
### Classs
考慮整數 $\mathbb{Z}$
$\{n\in \mathbb{Z}:\text{n is odd}\}$ 就是一個 class
也可記做
$[n\in\mathbb{Z}]_{\equiv2}=\{n\in \mathbb{Z}:\text{n is odd}\}$
### Partition and Quotient
Quotient 是一個 Partition，直接以例子來講的話就是
$$
\mathbb{Z}/\equiv_2\;=\{\{n\in\mathbb{Z}:\text{n is odd}\}, \{n\in\mathbb{Z}:\text{n is even}\}\}
$$
### Relation Refinement
考慮兩個 Relation $R_1,R_2$，我們說
$R_1\text{ is a refinement of }R_2$, $R_1\text{ refines }R_2$ 或著是 $R_1\prec R_2$ 代表
$$
\forall s_1,s_2\in S.s_1R_1s_2\rightarrow s_1R_2s_2
$$
### Congruence Closure
* Congruence closure is the smallest congruence relation that covers R
#### Subterm Set
$\Sigma_E$-formula 內 term 的集合
ex.
$F: f(a,b)=a\land f(f(a,b),b)\neq a$
$S_F=\{a,b,f(a,b),f(f(a,b),b)\}$
* **Example 1**: $F:f(a,b)=a\land f(f(a,b),b)\neq a$
1. `{{a}, {b}, {f(a, b)}, {f(f(a, b), b)}}`
2. `{{a, f(a, b)}, {b}, {f(f(a, b), b)}}`
(f(a, b) = a)
3. `{{a, f(a, b), f(f(a, b), b)}, {b}}`
(function congruence)
4. $T_E$-unsatisfiable
* **Example 2**: $F:f^3(a)=a\land f^5(a)=a\land f(a)\neq a$
1. `{{a}, {f(a)}, {f^2(a)}, {f^3(a)}, {f^4(a)}, {f^5(a)}}`
2. `{{a, f^3(a)}, {f(a)}, {f^4(a)}, {f^5(a)}}`
(f^3^(a) = a)
3. `{{a, f^5(a)}, {f(a), f^4(a)}, {f^2(a), f^5(a)}}`
(function congruence)
4. `{{a, f^2(a), f^3(a), f^5(a)}, {f(a), f^4(a)}}`
(f^5^(a) = a)
5. `{{a, f(a), f^2(a), f^3(a), f^4(a), f^5(a)}}`
(function congruence)
6. $T_E$-unsatisifiable
:::warning
DAG not done yet.
:::
# Hoare Logic
http://www.im.ntu.edu.tw/~tsay/
[課程](http://flolac.iis.sinica.edu.tw/flolac17/doku.php?id=course:smt)
這個
Coscup演講的題目XD
是為Command所造的公理系統
可以用來驗證程式的性質
我想直接利用之前的資料就可以了
[演講內容](https://github.com/KevinKu/Formal-verification-of-simple-C-code)
[演講補充](https://hackmd.io/s/r1Cu7pcwW)
[新南威爾斯大學課程](http://cs4161.web.cse.unsw.edu.au/lect.html)
額外說明Weakest Precondition and Strongest Postcondition和Verification Condition Generation
## Hoare Triples
基本形式:{P}C{Q}
P為前置條件(precondition)
C為指令(command)
Q為後置條件(postcondition)
簡單來說，就是我們在P的狀況，執行C指令，然後會有結果Q
## Proof Rules
## Total Corrctness
一般來說，如果我們每個Hoare triple 都符合我們的證明規則，那我們可以稱做 Partial Correctness. 而如果程式可以終止的話，則我們便有了Total Corrctness.
而total Correctness 定義如下:
如果我們有個 Hoare Triple {P}while B do S od {P $\land$ -B}且已經為Patial Correctness
如果我們可以建造個整數函數 t使得:
{P$\land $B$\land$ t=Z}S{t<Z} and P$\land$B$\to$t>0
則這個Hoare triple為Total Correctness
## An example
我們先看個關於while的程式:
sum=0,i=0
while(i<10){
sum = sum + i;
i = i+1;
}
然後我們可以使用Hoare logic 證明這個程式會得出sum=45。
我們先證明Partial Correctness
sum=0,i=0
{$sum =0 \land i=0$}
{$i<10\land sum=\sum_{k=0}^{i}k$}
while(i<10){
i=i+1
{$i<=10\land sum=\sum_{k=0}^{i-1}k$}
sum= sum+i
{$i<10\land sum=\sum_{k=0}^{i-1}k+i$}
{i<10\land sum=\sum_{k=0}^{i}k$}
}
{$i=10 \land sum=\sum_{k=0}^{i}k$}
{$sum=\sum_{k=0}^{9}k$}
{sum = 45}
至於Total correctness 我們可以 假設t=10-i便很容易能解出來了
## Weakest Precondition and Strongest Postcondition
:::info
對這樣的logic formula : $P \Rightarrow Q$ , 稱$P$比起$Q$ stronger , $Q$比起$P$ weaker
Weakest 與 Strongest 就是上述關係的極致
:::
這邊是這樣的
光是有rule, 還是不夠好做證明
於是一個自然的問題就來了
對於每個{P}C{Q}
C為基本的command
有沒有一些前置斷言或後置斷言
是恆成立且可以藉由rule消去Hoare triples
變成單純的logic formula
能讓這件事成立的前置斷言與後置斷言
分別稱作Weakest Precondition 與 Strongest Postcondition
## Verification Condition Generation
這邊補充Verification Condition Generation與Weakest Precondition , Strongest Postcondition的關係
Verification Condition Generation就是用每個command的rule , 分解成最基礎的command , 再利用Weakest Precondition 與 Strongest Postcondition生成logic formula的過程
## Symbolic Execution
# An Introduction to Automata Learning
若想對一個黑箱系統建模，有一個方法是觀察它的行為並用 automata 畫出來，考慮以下的例子。
:::info
以這個咖啡機的例子來說，投 15 塊就可以選擇咖啡或茶，在每個節點都可以按`↺`回到 0 的位置（這裡應該要畫，忘記畫）。因此可以觀察到以下的情況
* 10 5 Coffee (good)
* 10 10 Coffee (bad)
* 5 5 5 Tea (good)
* 5 `↺` 5 10 Coffee (good)
:::
* Finite automata: 從有限長度的字串 mapping 到 boolean values。
* Multiplicity automata: 從有限長度字串 mapping 到相對應的值，例如溫度，時間等。
* Büchi automata: 無限長度的字串 mapping 到 boolean value。
## L^*^ Learning Algorithm
```sequence
L* Algorithm->Teacher: Finite string s
Teacher-->L* Algorithm: Yes/No
Note right of Teacher: Membership Query
L* Algorithm->Teacher: DFA C
Teacher-->L* Algorithm: difference of L(C) and L
Note right of Teacher: Equivalence Query
```
上面的圖畫得還不是很好，但它的原理與猜數字的遊戲有些相似，它分成兩個部份`Membership Query` 及 `Equivalence Query`。有兩個角色`Teacher`已經知道一個 automata，而`L*`演算法要藉由一連串的問題準確猜出`Teacher`所知道的 automata 長得怎樣。
`Membership`問題是給一有限長度的字串，問`Teacher`該字串有沒有在它的 automata 內（是否會 terminate），而 `Teacher`就回答是或不是。
`Equivalence`則是`L*`根據前面的問題，畫出一個 automata 並問`Teacher`這個 automata 是否與`Teacher`的 automata 一樣，如果一樣，那恭喜，我們的`L*`在沒有任何資訊的情況下，準確猜出`Teacher`所想的 automata。但如果不一樣，`Teacher`就要給出一個反例，這個反例在`L*`給出的 automata 會結束，但在`Teacher`的 automata 不會結束，而`L*`就要根據反例再做一次`Membership`及`Equivalence`的問題流程，直到找出答案為止。
:::info
:::
`L*`演算法並不是一個很有效的方法，部份`Membership`問題是可以不用問的，還有一種用`classification tree`的方法，原理其實相同這裡不多介紹了。
### L^*^ Applications
像`L*`這樣的 automata learning 的演算法最大的好處是可以藉由觀察一個黑箱系統的行為，進而建構出其 automata 模型。
:::danger
Multiplicity Automata
Non-terminating System
:::
## Non-terminal Automata
# Synthesis
> [詳細版的投影片](http://cc.ee.ntu.edu.tw/~jhjiang/instruction/courses/fall14-lsv/lec01_2p.pdf)
> [name=Yen-Kuan Wu][color=#8c66c9]
首先先來看看 logic synthesis 在 IC design flow的哪個部份
沒錯就是從 logic netlist 準備到 circuit netlist 的時期所做的優化，試想一個問題，不同的邏輯扎電路有可能等價於其他且使用到更少邏輯閘的邏輯電路，而 Formal 也可以使用在這邊，可以判斷這兩組電路是否等架，或者是有沒可能 output永遠是 0 之類的，接下來我們先介紹 Booelan function跟為何要從 logic circuit 轉換到 boolean function，轉換過後在透過 Boolean Satisfiability這項技術來做所謂的驗證。
:::info
補充
* [IC Design Flow](http://access.ee.ntu.edu.tw/course/under_project_94/pdf/20060308_ic_design_flow.pdf#page=22)
:::
## Boolean Satisfiability
### Boolean Function
Boolean Function 就是一個函數 $f: \textbf B^k\rightarrow \textbf Y$，其中 $\textbf B=\{0,1\}$是布林域，$\textbf Y=\{0, 1, d\}$, $d$是 don't care的意思，也就是 0 或 1都行。
> let k = 2, $\textbf B^2 = \{0,1\}*\{0,1\}=\{00,01,10,11\}$。
再來舉個例子，
$f(x_1,x_2) = x_1$ 的 output 可以分成以下 3 種情況：
> 注意，$x_1+x_2+x_1x_2$的 + 在布林代數上其實是 AND的意思，相乘也就是 OR[name=Yen-Kuan Wu][color=#4d21b2]
* **onset** of$f$ 定義成 $f^1=\{v\in B^n|f(v)=1\}$
eg. $f^1=\{10,11\}$
* **offset** of $f$ 定義成 $f^0=\{v\in B^n|f(v)=0\}$
eg. $f^0=\{00, 01\}$
* **don't-care-set of $f$** 定義成 $f^d=\{v \in B^n|f(v)=?\}$
eg. $f^d=\{00,01\}$
> 如果 f的 don't-care set 不會空集合，我們就說 f是 incompletely specified function，反之，f 就是 ==completely specified function==，這邊我們都是指 completely specified function[name=Yen-Kuan Wu][color=#4d21b2]
> $f^1=\textbf B^n$ iff $f$ is **tautology**.
> $f^0=\textbf B^n$ iff $f$ is **unsatisfiable**. Otherwise, f is **statisfiable**.[name=Yen-Kuan Wu]
接著定義一些常用的用語
> Boolean function f and g are **equivalent** if $\forall v \in \textbf B^n. f(v) = f(v)$ where v is a truth assignment or Boolean valuation.
>
> A **literal** is a Boolean varaible $x$ or its negation $\neg x$[name=Yen-Kuan Wu][color=#4d21b2]
再來我們進入 Boolean的操作
> 給定兩個 Boolean function
> $$
> f: \textbf B^n \rightarrow \textbf B\\
> g: \textbf B^n \rightarrow \textbf B
> $$
> **AND** ops: $h = f \land g$ is defined as $h^1 = f^1 \cap g^1$
> **OR** ops: $h = f \lor g$ is defined as $h^1 = f^1 \cup g^1$
> **COMPLEMEN** ops: $h = \neg f$ is defined as $h^1 = f^0, h^0 = f^1$
> [name=Yen-Kuan Wu][color=#4d21b2]
給定 $f$ 的 input variable $(x_1, x_2, ... , x_i, ... , x_n)$
* Positive cofactor on variable $x_i$
* $f_{xi}=f(x_1,x_2,..,1,..,x_n)$
* Negative cofactor on variable $x_i$
* $f_{\lnot xi}=f(x_1,x_2,..,0,..,x_n)$
* Existential quantification over variable $x_i$
* $\exists x_i.f=f(x_1,x_2,..,0,..,x_n)\lor f(x_1,x_2,..,1,..,x_n)$
* Universal quantification over variable $x_i$
* $\forall x_i.f=f(x_1,x_2,..,0,..,x_n)\land f(x_1,x_2,..,1,..,x_n)$
* Boolean difference over variable $x_i$
* ${\partial f/ \partial x_i}=f(x_1,x_2,..,0,..,x_n)\oplus f(x_1,x_2,..,1,..,x_n)$
> $\oplus$ = XOR[name=Yen-Kuan Wu][color=#fcc7fa]
再來我們要介紹 Boolean formula
$$
formula := (formula)\ |\ Boolean \ constant\ (true\ or\ false)\ |\ Boolean\ variable\ |\\
formula\ "+"\ formula\ (OR\ operation)\ | formula "*" fomula (AND\ operation)\ |\\
\neg formula\ (Completement operation)
$$
> e.g. $f = x_1 + x_2 + x_1 * x_2$
:::info
有幾種表達 Boolean Functions 的形式，會視不同的應用有好與壞處。
* Truth table
* Boolean formula
* SOP (sum-of-products, or disjunctive normal form, DNF)
* POS (product-of-sums, or conjunctive normal form, CNF)
* **BDD** (binary decision diagram)
* Boolean Network
* Generic Boolean Network
* And-Inv Graph (**AIG**)
詳細的表達式可參考投影片 P.14 開始。 (BDD, AIG 是重點)
http://cc.ee.ntu.edu.tw/~jhjiang/instruction/flolac11.pdf
:::
這邊會提一些重要的表達型式(representation)
* Truth table
> 我想 truth table我也不用多提什麼了，但這邊我要介紹一個很重要的性質
>
> 如果這個 represetation 是 **canonical** 那麼兩個 equivalent 的 function 的 會有相同的 representation
>
> 而 truth table 正是 canonical represetation[name=Yen-Kuan Wu][color=#4d21b2]
* Sum-of-products
* any function can be represented as a ==sum-of-products(SOP)==, also called ==sum-of-cubes (a cube is a product term)==, or **==disjunctive normal form(DNF)==**
* e.g. $\varphi = ab + a'c$
* Product-of-sums
* any function can be represented as ==product-of-sum(POS)== also called **==conjuctive normal form(CNF)==**
* e.g. $\varphi = (a + b)(a + c')$
* Binary Decision Diagram(BDD)
* 我們會發現 BDD並不是 canonical(左邊和右邊的樹狀圖)，同一個 function 有不同的 representation
:::info
緊接著我們要介紹兩個用來描述 BDD的性質，reduced 和 ordered
Ordered BDD 就是所有由 top 到 leaf的 path 都符合一定的順序
Reduced BDD 意思是把可以化簡的都化簡了，e.g. 由於 Node a 是 true or false 都會接到 Node b，所以基本上就可以省略
由這兩個性值得出的 BDD，Reduced and Ordered BDD (ROBDD) 就擁有 canonical 的特性，所以我們可以安心使用
:::
* And-Inv Graph (AIG)
:::info
各表達式的的特性
* Truth Table
* Canonical
* Useful in representing small functions
* SOP
* Useful in 2-level logic optimization, and in representing local node functions in a boolean network.
* POS
* Useful in SAT solving and Boolean reasoning
* Rarely used in circuit synthesis
* ROBDD
* Canonical
* Useful in Boolean reasoning
:::
https://people.eecs.berkeley.edu/~alanmi/abc/
## Propositional Satisfiability
#### Normal Forms
* Conjunctive normal form (CNF): conjunction of clauses
* $(a+\lnot b+c)(a+\lnot c)(b+d)(\lnot a)$
* Disjunctive normal from (DNF): disjunction of cubes
* $a\lnot bc+a\lnot c+bd+\lnot a$
### Satisfiability
SAT 是給一個 CNF 問是否存在一組能使 CNF 為真的解，演算法計算理論那章說 SAT 是一個 NP-complete 問題。
但現在的 SAT solvers 就算處理約 10 萬個變數及 100萬個 clauses 也能有不錯的效率。常用的 SAT solvers 有：
* DPLL-style search
* Conflict-driven clause learning (CDCL)
* Boolean constraint propagation (BCP) with two-literal watch
* Decision heuristics using variable activity
* Restart
* Preprocessing
* Support for incremental solving ([MiniSat](http://minisat.se/))
:::danger
各個方法的介紹可以參考台大電子所江介宏老師的[投影片](http://cc.ee.ntu.edu.tw/~jhjiang/instruction/flolac11.pdf)，第 35 頁開始。
DPLL and Resolution
:::
## SAT & Logic Synthesis
### Equivalence Checking
```graphviz
digraph hierarchy {
graph [rankdir = LR, splines=ortho];
node[shape=none]
x1[label="x"];
x2[label="x"];
y1[label="y"];
y2[label="y"]
node[shape=triangle, orientation=270]
C1;
C2;
x1->C1->y1;
x2->C2->y2;
}
```
假設有兩個電路 C1 及 C2，我們要如何說它是相等的?
在最後面加上 XOR gate 去判斷 output 是否相等。
:::danger
XOR gate 的圖還不會畫
:::
### Functional Dependency
Functional Dependency 最主要的作用就是減少電路面積，我們說
$$
f(x)\text{ functionally depends on }g_1(x),g_2(x),g_3(x)...g_n(x)\text{可以表示為}h(G(x))
$$
如果$h$存在，則可以說
$$
h\text{ exists}\Leftrightarrow\nexists a,b\text{ such that }f(a)\neq f(b)\text{ and }G(a)=G(b)
$$
```graphviz
digraph hierarchy {
graph [rankdir = LR, splines=ortho];
node[shape=ellipse]
X; Y; Z;
X->Z[label="f"];
X->Y[label="G"];
Y->Z[label="h"];
}
```
至於為什麼原本好好的$f(X)$要多經過一道程序$h(G(X))$?
source 江介宏老師的[投影片](http://cc.ee.ntu.edu.tw/~jhjiang/instruction/flolac11.pdf) p.49
:::danger
BDD-Based Computation
:::
# Verification of String Manipulating Programs(Web Application)
[課程投影片](http://www3.nccu.edu.tw/~yuf/slides/string.pdf)
相信各位已經知了，網頁應用程式可以說是生活中不可或缺的，而且我們常常會使用網頁應用程式，e.g. 逛逛FB, 繳費，甚至處理公務，而網頁應用程式的數量理所當然是數以萬計，那數以萬計的程式就有數以萬計的 bugs = =|||。
網頁應用程式、手機APP...這類型的互動式應用程式往往是非常容易有漏洞的，而且往往駭客用透過網頁應用程式駭入 server後，就會造成網頁的使用者或是會員集體受到侵犯，不得不說，網頁應用程式的安全很重要。
網頁自然會使用到大量的字串操作，不外乎顯示網頁內容、互動、資料庫存取，很容易有漏洞，因為你無法預期時使用者輸入什麼字串或是點選不合理的位置。
讓我們來看看幾個常見的攻擊手法。
### SQL Injuction
注入式攻擊，也稱 Injection flaws 或 SQL Injuction，以下是PHP的範例：
```php=
<?php
$name=$_GET["name"];
$usr_data=$db->query('SELECT * FROM students WHERE name = "$name"');
?>
```
如果我們輸入 Jserv'); DROP TABLE students; --，那會怎樣呢？
```php=
<?php
$name=$_GET["name"];
$usr_data=$db->query('SELECT * FROM students WHERE name = "Jserv'); DROP TABLE students; --');
?>
```
這不就是一個很危險的漏洞嘛！？
### Cross Site Scripting Attack
跨站式腳本攻擊，Cross site scripting attack 簡稱 XSS，這個漏動能使駭客住入一個惡意程式來入侵 server，大家要注意，如果入侵server代表說他能夠入侵使用者的資料甚至是從server來入侵使用者，這也是為什麼會有跨站式之稱，提外話如果是透過公用API來入侵的話是無法有效區分惡意攻擊者的，何況換個IP就好。
一樣是 php的範例：
```php=
<?php
$www = $_GET["www"];
$info = "URL";
echo "<td>" . $info . ":" . $www. "</td>";
?>
```
此時我們將輸入 <script ...> 來迫使 server 執行惡意script
```php=
<?php
$www = <script ...>;
$info = "URL";
echo "<td>" . $info . ":" . <script ...> "</td>";
?>
```
我們先來用一個分析方式叫作 taint analysis[1]，他會先尋找弱點變數，在本例就是這行`$www = $_GET["www"]`，再來去用到這個弱點變數尋找危險函數，那就是這行 `echo "<td>" . $info . ":" . <script ...> "</td>"`
我們新增 sanitization routine來預防看看 (#3 也就是把不應該出現的字符填成空字符)
```php=
<?php
$www = $_GET["www"];
$info = "URL";
$www = ereg_replace("[^A-Za-z0-9 .-@//]", "", $www);
echo "<td>" . $info . ":" . $www. "</td>";
?>
```
這邊其實有一個 bug是 ".-@"，他會視為'.'到 '@'，由於這個 bug，我們就能這樣破解，<!sc+ript ...>，經過那行函式後又變回 <script ...>，所以這其實真的很難防，還是乖乖來做 formal分析吧
## Web Application 的脆弱之處
* 跨站腳本攻擊(XSS)
* 注入弱點(例如:SQL Injuction)
## 為什麼有 Web Application 的錯誤傾向?
由於廣泛的字串使用:
* Web Application 廣泛的使用字串(EX.創建網頁)
## String Analysis
* 字串分析決定了所有可能
* 主要的想法是把字串看成某個automata的language
## 困難之處
* 精準度
* 複雜度
* 效能
## A Language-based Replacement
### 定義
M = REPLACE($M_1,M_2,M_3$)
* $M_1,M_2,M_3$ are DFAs.
* $M_1$ accepts the set of orginal string.
* $M_2$ accepts the set of match string
* $M_3$ accepts the set of replacement string.
Ex.L($M_1$)={baab},L($M_2$)=$a^+$,L($M_3$)={c}
L(M)={bcb,bccb}
### 在電腦上的操作
# Vienna Development Method
# Blockchain
digital currency 數位貨幣
FinTech - financial technology
delivery of financial service
make efficient
Gartner Hype Cycle
digi moneny
counterfeit: cryptograph: **digital signature**
blockchain **immutable ledger**
[blockchain原理Demo](https://anders.com/blockchain/)
可以在上面網站使用 , 會示範整個blockchain的狀態
Sign in with Wallet
Connect another wallet