# LTL 驗證算法疑問
## proof.K
---
# LTL Formula
* base on Propositional Logic ($\land$ $\lor$ $\rightarrow$ $\leftrightarrow$)
* **X**a (Next)
* **G**a (Globally)
* **F**a (Finally)
* a **U** b (Until)
* a **W** b (Weak until)
* a **R** b (Release)
---
# $M,s \vDash P$
* **M** is <font color="#449df9">transition system</font> (model)
* **s** is <font color="#449df9">state</font>
* **P** is <font color="#449df9">LTL formula</font>
---
# Transition System (model)
## $M = (S,\rightarrow,L)$
* **S** is set of states
---
# $M = (S,\rightarrow,L)$
## $\rightarrow$ is transition relation
* $(a,b) \in \rightarrow$ : $a,b$ are <font color="#449df9">state </font>
* $(a,b)$ : $a \rightarrow b$
---
# $M = (S,\rightarrow,L)$
## $L$ is <font color="#449df9">labelling function</font>
* $L$ : $S \rightarrow 2^{Atoms}$
* $2^{Atoms}$ is <font color="#449df9">LTL formula set</font>
* $f \in L(a)$ : $f$ is true in <font color="#449df9">state a</font>
---
# $M = (S,\rightarrow,L)$ (Transition System) is Graph
```graphviz
digraph a {
fontname="Helvetica,Arial,sans-serif"
node [fontname="Helvetica,Arial,sans-serif"]
edge [fontname="Helvetica,Arial,sans-serif"]
a[label="p,q"]
b[label="r"]
c[label="p"]
a -> a
a -> b
b -> c
c -> a
}
```
---
# $M,s \vDash P$
## $M,s \vDash P$ if for every path $\pi$ of $M$ starting at $s$ , we have $\pi \vDash P$
---
# $\pi \vDash P$
## path
```graphviz
digraph a {
fontname="Helvetica,Arial,sans-serif"
node [fontname="Helvetica,Arial,sans-serif"]
edge [fontname="Helvetica,Arial,sans-serif"]
a[label="{p,q} a"]
b[label="{r} b"]
c[label="{p} c"]
a -> a
a -> b
b -> c
c -> a
}
```
bcaaaa..... is a path starting at b
---
# $\pi \vDash P$
* $\pi \vDash \top$
* $\pi \not \vDash \bot$
* $\pi \vDash P$ if $P \in L(s)$
```graphviz
digraph a {
fontname="Helvetica,Arial,sans-serif"
node [fontname="Helvetica,Arial,sans-serif"]
edge [fontname="Helvetica,Arial,sans-serif"]
a[label="{P,q} s"]
a -> a
}
```
---
# $\pi \vDash P$
* if $\pi \not \vDash P$ , then $\pi \vDash \neg P$
* if $\pi \vDash a$ and $\pi \vDash b$ , then $\pi \vDash a \land b$
* if $\pi \vDash a$ or $\pi \vDash b$ , then $\pi \vDash a \lor b$
---
# $\pi \vDash P$
* if $\pi \vDash b$ whenever $\pi \vDash a$ , then $\pi \vDash a \rightarrow b$
---
# $\pi \vDash P$
* if $\pi^{1} \vDash p$ , then $\pi \vDash X \ p$
---
# $\pi^{1} \vDash p ?$
* $\pi = s_{0}s_{1}s_{2}s_{3}s_{4}s_{5}...$
* $\pi^{1} = s_{1}s_{2}s_{3}s_{4}s_{5}...$
* $\pi^{4} = s_{4}s_{5}...$
---
# $\pi \vDash X \ p$
$\pi = sdf$
$\pi \vDash X \ a$
```graphviz
digraph a {
rankdir = LR
fontname="Helvetica,Arial,sans-serif"
node [fontname="Helvetica,Arial,sans-serif"]
edge [fontname="Helvetica,Arial,sans-serif"]
s[label="{P,q} s"]
d[label="{a} d"]
f[label="{b} f"]
s -> d
d -> f
}
```
---
# $\pi \vDash P$
* if $\pi^{i} \vDash p$ for every $i \ge 0$ , then $\pi \vDash G \ p$
$\pi = sdfgj$
$\pi \vDash G \ p$
```graphviz
digraph a {
rankdir = LR
fontname="Helvetica,Arial,sans-serif"
node [fontname="Helvetica,Arial,sans-serif"]
edge [fontname="Helvetica,Arial,sans-serif"]
s[label="{p,q} s"]
d[label="{p,a} d"]
f[label="{p,b} f"]
g[label="{p,e} g"]
j[label="{p,v} j"]
s -> d
d -> f
f -> g
g -> j
}
```
---
# $\pi \vDash P$
* if $\pi^{i} \vDash p$ for some $i \ge 0$ , then $\pi \vDash F \ p$
$\pi = sdfgj$
$\pi \vDash F \ b$
```graphviz
digraph a {
rankdir = LR
fontname="Helvetica,Arial,sans-serif"
node [fontname="Helvetica,Arial,sans-serif"]
edge [fontname="Helvetica,Arial,sans-serif"]
s[label="{p,q} s"]
d[label="{p,a} d"]
f[label="{p,b} f"]
g[label="{p,e} g"]
j[label="{p,v} j"]
s -> d
d -> f
f -> g
g -> j
}
```
---
# $\pi \vDash P$
* $\pi \vDash a \ U \ b$ if there is some $i \ge 0$ such that $\pi^{i} \vDash b$ and for every $i > j \ge 0$ , $\pi^{j} \vDash a$
$\pi = sdfgj$
$\pi \vDash p \ U \ e$
```graphviz
digraph a {
rankdir = LR
fontname="Helvetica,Arial,sans-serif"
node [fontname="Helvetica,Arial,sans-serif"]
edge [fontname="Helvetica,Arial,sans-serif"]
s[label="{p,q} s"]
d[label="{p,a} d"]
f[label="{p,b} f"]
g[label="{e} g"]
j[label="{e,v} j"]
s -> d
d -> f
f -> g
g -> j
}
```
---
# $\pi \vDash P$
* $\pi \vDash a \ W \ b$
$\pi \vDash a \ U \ b$ or $\pi \vDash G \ a$
---
# $\pi \vDash P$
* $\pi \vDash a \ R \ b$
$\pi \vDash G \ b$ or if there is some $i \ge 0$ such that
$\pi^{i} \vDash a$ and for every $i \ge j \ge 0$ we have $\pi^{j} \vDash b$
```graphviz
digraph a {
rankdir = LR
fontname="Helvetica,Arial,sans-serif"
node [fontname="Helvetica,Arial,sans-serif"]
edge [fontname="Helvetica,Arial,sans-serif"]
s[label="{p,q} s"]
d[label="{p,a} d"]
f[label="{p,e,b} f"]
g[label="{p,e} g"]
j[label="{p,e,v} j"]
s -> d
d -> f
f -> g
g -> j
}
```
$\pi = sdfgj$
$\pi \vDash e \ R \ p$
{"title":"LTL 驗證算法疑問","contributors":"[{\"id\":\"ba6061cd-562a-4173-a475-cffdd5651baf\",\"add\":5447,\"del\":162}]","description":"base on Propositional Logic (==\\land \\lor \\rightarrow $\\leftrightarrow:w"}