[Model Checking] Linear Time Properties

이 글은 RWTH AACHEN 대학교 Joost-Pieter Katoen 교수님의 2018년 1학기 Introduction to Model Checking 강의와 Principles of Model Checking을 기반으로 재구성한 것입니다.

 model checking의 주된 알고리즘은 transition system과 requirement를 model checker에 넣어, 해당 transition system이 requirement를 만족하는지 여부를 확인하는 방법이다. 그래서 지금까지 transition system을 모델링하는 방법을 살펴봤었고, 지금부터는 requirement를 모델링하는 방법을 살펴볼 것이다.

 

 이 포스트에서는 크게 4가지를 살핀다.

• state-based and linear time view
• definition of linear time properties
• invariants and safety
• liveness and fairness

 

 

 

State Graph

 transition system TS는 (S, Act, → I, AP, L)의 tuple로 표기한다. 여기서 Act는 interaction, communication을 modeling하고 fairness를 설명할 때 쓴다. 반면 AP와 L은 properties를 정의할 때 쓴다. 따라서 일단 properties를 다룰 때는 labeling과 state만 일단 신경쓴다.

 

Definition. State Graph

 state graph G$_{T}$를 정의하자. transition system TS가 (S, Act, → I, AP, L)일 때, G$_{T}$의 node는 S와 동일하고, edge는 action label이 없는 transition이다.

 

Definition. Path Fragment

 이전 포스팅에서 execution fragment, initial execution fragment, maximal execution fragment에 대해 살펴봤었다. path fragment는 이와 유사한 개념으로 graph에서 정의되는 execution fragment라 생각하면 된다. TS를 G$_{T}$로 바꿨던 것처럼 execution fragment는 $\pi$=$s_0s_1s_2$...such that s$_{i+1}$ ∈ Post(s$_i$) for all i in |$\pi$|로 정의한다.

 

• initial path fragment는 s$_0$ ∈S$_0$인 경우를 말한다. (initial state에서 시작한다는 뜻이다.)
• maximal path fragment는 infinite거나 terminal state에서 끝나는 path fragment를 말한다. 

 transition system execution이 initial & maximal execution fragment였던 것처럼, 동일하게 transition system path는 initial & maximal path fragment이다.

 

 추가로, 편의를 위해 어떤 state s의 path를 s에서 시작하는 maximal path fragment라 정의하자. 또한 Paths(T)는 transition system의 가능한 모든 path의 집합을, Paths(s)는 state s에서 시작하는 모든 maximal path fragment들의 집합이라 정의하자. Paths$_{\text{fin}}$(s)는 s에서 시작하는 모든 finite path fragment $\hat{\pi}$들의 집합이라 정의하자.

 

Linear Time View vs Branching Time View

 바로 위에서 transition system T를 state graph와 state에 대한 labeling으로 나누었다.

 linear time view는 path-based이다. state sequence만 보면 모든 것을 알 수 있다는 뜻이다. branching의 경우, 각 branching의 결과를 state sequence로 볼 수 있기 때문에 branching과 관련이 없다. action을 abstract하고 AP에 투영한다. 이를 trace라 한다.

 branching time view는 nondeterministic branch에 대해 설명하므로 state와 branch를 abstraction한다. 이를 computation tree라 한다.

 

 

 

Trace

path는 $\pi$=$s_0s_1s_2$였는데, 이 path의 각 state에 대한 atomic proposition을 적용한 L(s$_0$)L(s$_1$)L(s$_2$)를 trace라 한다. trace는 labeling의 sequence이므로 ($2^{\text{AP}}$)$^{\omega}$ ∪ ($2^{\text{AP}}$)$^{+}$에 속한다.

 

개선: Terminal State 삭제

 이러한 표현은 식이 너무 더럽기 때문에 TS에 terminal state가 없다고 가정하기도 한다. terminal state가 없다면 모든 경우에서 finite에 대한 계산을 없앨 수 있다. (모든 경우가 infinite)

 

 기존 terminal state에서 자기 자신으로 가는 edge 하나를 추가하는 방식으로 terminal state를 없앤다.

• 예를 들어, 프로그램이 의도했던 종료 상태 s로 가는 transition system을 생각해 보자. 모든 reachable terminal state s에 대해 특별한 stop state로 edge를 추가해 기존 s를 terminal state가 아니게 하고, stop state는 자기 자신으로 edge를 추가하면 terminal state가 없어졌으므로 path가 infinite하게 된다.
• 다른 경우는 system fault로 인한 부분이다. 이 경우는 terminal이 되기를 원하지 않지만 system fault나 deadlock에 의해 멈추는 경우는 프로그램의 설계가 잘못되었으므로 이를 수정해야 한다.

 

 Traces(T)를 transition system T의 모든 path $\pi$들의 trace의 합집합이라고 하자. 수식으로 정의하면 Traces(T) := {traces($\pi$) : $\pi$ ∈ Paths(T)}이고, 이 때 $\phi$는 initial & maximal path fragment이다. Traces(T) ⊆ ($2^{\text{AP}}$)$^{\omega}$이다.

 같은 방법으로 Traces$_\text{fin}$(T) := {traces($\hat{\pi}$) : $\hat{\pi}$ ∈ Paths$_\text{fin}$(T)}라고 정의하자. 이 때 $\hat{\pi}$는 initial & finite path fragment이다. Traces$_\text{fin}$(T) ⊆ ($2^{\text{AP}}$)$^{*}$이다.

 만약 terminal state를 삭제한 경우에는 무조건 infinite가 된다는 점을 유의하자.

 

 

 

Linear Time Property

 앞서 model checker는 transition system T와 requirement를 구체화한 spec으로 T가 spec을 만족하는지 여부를 확인하는 기계라고 했다. 여기서 spec중 하나가 linear time property이다!

 

 atomic propisition의 집합 AP에 대한 linear time property는 ($2^{\text{AP}}$)$^{\omega}$의 부분집합이다. 즉, state의 labeling의 infinite word의 부분집합이라는 뜻이다. 

 

Definition. Satisfaction Relation for Linear Time Property

 transition system이 언제 linear time property를 만족하는지 알 수 있어야 한다.

 어떤 transition system TS와, TS의 atomic proposition AP, AP의 linear proposition E에 대해 Traces(T) ⊆ E iff TS $\models$ E이다. transition system의 모든 path의 trace가 E에 속할 때, transition system TS가 E를 만족하고 그 역도 성립한다는 것을 의미한다.

 state에 대해서도 이를 정의하는데, s가 TS의 state일 때 Traces(s) ⊆ E iff s $\models$ E이다.

 

Definition. Trace Inclusion and Linear Time Properties

 T$_1$과 T$_2$가 AP에 대한 transition system이고, AP에 대한 linear time property가 E에 대해 Traces(T$_1$) ⊆ Traces(T$_2$) iff T$_2$ $\models$ E then T$_1$ $\models$ E이다.

 

trace inclusion은 아래 3가지 영역에서 나타난다.

• implementation / refinement relation : 예를 들어 어떤 transition system T$_i$가 LT property E를 만족한다고 했을 때, T$_i$를 조금 수정한 T$_{i+1}$이 있다고 하자. 이 때 T$_{i+1}$ ⊆ T$_i$라면 T$_{i+1}$도 E를 만족한다는 것을 보일 수 있다.
• resolving nodeterminisim : 예를 들어 어떤 scheduling policy에서 nondeterministic한 선택을 하는 T에서 deterministic 한 선택을 하는 T'을 만들었다고 하자. 이 때 Traces(T') ⊆ Traces(T)이므로 T가 E를 만족하면 T'도 E를 만족하는 것을 보일 수 있다.
• data abstraction : 원래 transition system T의 data를 추상화해 transition system T'를 만들었다고 하자. T'가 더 상위의 개념이므로 T의 모든 data들은 T'를 만족한다. Traces(T) ⊆ Traces(T')이므로, T'가 E를 만족하면 T도 E를 만족한다.

 

Definition. Trace Equivalance

 같은 atomic proposition AP에 대한 transition system T$_1$, T$_2$가 있을 때 Traces(T$_1$) = Traces(T$_2$) iff trace equivalance이다.

 앞선 Trace Inclusion and LT Properties에 의해 transition system이 trace equivalent하면 동일한 linear time property를 만족한다. T$_1$과 T$_2$가 AP에 대한 transition system이고, AP에 대한 linear time property가 E에 대해 Traces(T$_1$) = Traces(T$_2$) iff 모든 LT property E에 대해 T$_2$ $\models$ E then T$_1$ $\models$ E이다.

 

 

 

Safety Properties and Invariants

 그럼 이제 linear time property를 분류하자.

 safety properties는 `나쁜 상태가 일어나지 않는 것`을, liveness properties는 `좋은 상태가 일어나는 것`을 의미한다.

• safety properties 예시 : deadlock이 일어나지 않는 것. critical section에 한 번에 2개 이상의 process가 접근하지 않는 것. 신호등의 red는 yellow가 선행한다. 등등.
• liveness properties 예시 : wait 상태에 들어간 process는 언젠가 critical section에 진입하는 것.

 이 때 safety properties 중 special case가 invariants이며, 어떤 나쁜 state에 도달하지 않는 것을 의미한다. 

 

 

Invariant

 AP에 대한 LT property E가 다음 조건을 만족하는 propositional fomula $\phi$가 존재할 때 E를 invariant라 한다.

 

E = {A$_0$A$_1$A$_2$... ∈ ($2^{\text{AP}}$)$^{\omega}$ : $\forall$ i ≥ 0. A$_i$ $\models$ $\phi$}

 

 이 때 $\phi$를 E의 invariant condition이라 한다.

 이 수식이 의미하는 것은 모든 trace의 모든 node가 $\phi$를 만족할 때, 이다. 

 

 이 때, invariant E에 대해 T $\models$ E와 다음 3가지는 동치이다.

1. iff trace($\phi$) ∈ E for all path $\phi$ ∈ Paths(T)
2. iff s $\models$ $\phi$ for all states s on a path of T
3. iff s $\models$ $\phi$ for all states s ∈ Reach(T)

 의미하는 것은 다음과 같다.

1. transition system T가 invariant LT property E를 만족한다면 transition system의 어떤 path를 고르더라도 trace($\phi$)가 E를 만족하는 것을 의미한다.
2. T의 path의 모든 state s가 $\phi$를 만족하는 것을 의미한다.
3. T의 모든 reachable state s가 $\phi$를 만족하는 것을 의미한다. 

 

Invariant Model Checking

자. 그럼 invariant를 쓸 때 model checker의 알고리즘을 얘기해 보자. model checker는 transition system T와 invariant LT property E를 받는다. model checker는 T가 E를 만족하는지 살핀다. 만약 만족한다면 true를, 그렇지 않다면 error를 나타낸다. 이 방법은 graph에서 DFS/BFS를 돌려 Reach(T)의 모든 state에 대해 s가 $\phi$를 만족하는지 살핀다. 만약 만족하면 true, 아닌 경우 error이다. pseudo code로 표현하면 다음과 같다.

FOR ALL s$_0$ ∈ S$_0$ DO     IF DFS(s$_0$, $\phi$) THEN         return "no"     FI OD return "yes"

 

DFS(s$_0$, $\phi$는 s$_0$에서 DFS를 했을 때 $\phi$를 만족하면 true를, 아닌 경우 false를 리턴하는 함수이다. 이 pseudo code를 수정해 어떤 path의 어떤 state에서 error가 났는지도 쉽게 찾을 수 있을 것이다.

IF s $\notin$ U THEN     IF s $\not\models$ $\phi$ THEN return "true" FI     IF s $\models$ $phi$ THEN         insert s in U         FOR ALL s' ∈ Post(s) DO             IF DFS(s', $\phi$) THEN                 return "true"             FI         OD     FI FI return "false"

 

 

Safety Property

 safety properties는 nothing bad will happen - 원치 않는 상태로 가지 않는 것을 보장한다.

 invariant는 bad state에 도달하지 않는 것을 의미하고 invariant가 아닌 safety properties는 bad prefix가 없는 것을 의미한다. 사실상 invariant는 safety properties의 special case라는 것을 생각하자.

 

 수식으로 정의해 보자. E가 AP에 대한 LT property라고 하자. 즉, E ⊆ ($2^{\text{AP}}$)$^{\omega}$일 때, $\sigma$ = A$_0$A$_1$A$_2$... ∈ ($2^{\text{AP}}$)$^{\omega}$ \ E에 대해 A$_0$A$_1$...A$_n$B$_{n+1}$B$_{n+2}$... 중 어떤 것도 E에 속하지 않도록 하는 $\sigma$의 finite prefix A$_0$A$_1$...A$_{n}$이 존재할 때, 이 조건을 만족하는 E를 safety property라고 한다.

 해석하자면 E에 없는 prefix를 어떻게 확장하더라도 E에 속하지 않는 property가 safety property이다. 즉... A$_0$A$_1$...A$_n$로 시작하는 word가 safety property에 속해야 한다는 것이라 보면 된다.

 

 수식으로 표현하면 E( = P$_\text{safe}$) ∩ {$\sigma$\ ∈ ($2^{\text{AP}}$)$^{\omega}$ | $\hat{\sigma}$는 $\sigma$'의 finite prefix} = $\phi$, 이 때 $\hat{\sigma}$는 bad prefix이며 bad prefix로 시작하는 word와 E의 합집합이 공집합이어야 한다는 뜻으로 의미는 같다.

 

BadPref

 bad prefix의 집합을 BadPref라고 한다.

 minimal bad prefix는 word의 bad prefix 중 제일 짧은 bad prefix를 의미한다.

 

Definition. Satisfaction Relation for Linear Time Property

 앞서 Satisfaction Relation for Linear Time Property에서 어떤 transition system TS와, TS의 atomic proposition AP, AP의 linear proposition E에 대해 Traces(T) ⊆ E iff TS $\models$ E라는 것을 살폈다. 여기에 추가로 붙는 iff 명제들이 있다.

TS $\models$ E

• iff TS $\models$ E
• iff Traces$_\text{fin}$(T) ∩ BadPref = $\phi$
• iff Traces$_\text{fin}$(T) ∩ MinBadPref = $\phi$
  • T의 finite trace 중 BadPref가 없다는 뜻이다.

 

Corollary

• 모든 invariant는 safety property이다. invariant는 safety property의 special case이다. 앞서 invariant는 bad state가 없는 것을, safety property는 bad prefix가 없는 것을 의미한다고 했다. bad state 또한 bad prefix로 표현할 수 있으므로, 부분집합이다.
• $\phi$는 safety property이다.
• ($2^{\text{AP}}$)$^{\omega}$는 safety property이다. 

 

Prefix Closure

 infinite word $\sigma$를 A$_0$A$_1$...라고 뒀을 때, pref($\sigma$)를 $\sigma$의 finite prefix의 집합으로, LT property pref(E)를 $\bigcup_{\sigma in E}^{}$pref($\sigma$)라고 정의하자. 이 때 closure(E)를 {$\sigma$ ∈ ($2^{\text{AP}}$)$^{\omega}$ pref($\sigma$) ⊆ pref(E)}라고 정의한다.

 해석하자면 모든 prefix pref($\sigma$)가 pref(E)에 속하는 모든 $\sigma$를 말하는 것이다.

 

Corollary

 E가 safety property iff closure(E) = E이다.

 E가 closed이므로 closure를 적용해도 같다.

 증명은 생략.

 

 

Finite Trace Equivalence

 앞서 Trace Inclusion and Linear Time Properties에서 T$_1$과 T$_2$가 AP에 대한 transition system이고, AP에 대한 linear time property가 E에 대해 Traces(T$_1$) ⊆ Traces(T$_2$) iff T$_2$ $\models$ E then T$_1$ $\models$ E이다.라고 했었다. 이는 finite trace에도 똑같이 적용된다.

Traces$_{\text{fin}}$(T$_1$) ⊆ Traces$_{\text{fin}}$(T$_2$) iff T$_2$ $\models$ E then T$_1$ $\models$ E이다.

 

 한편, Traces$_{\text{fin}}$(T)는 Traces(T)의 nonempty prefix의 집합, 즉 pref(Traces(T))이다!

 

Corollary

Traces(T) ⊆ Traces(T') then Traces$_{\text{fin}}$(T) ⊆ Traces$_{\text{fin}}$(T')이다.

 

Q.

trace equivalence iff finite trace equivalence인가? no.

Traces(T) ⊆ Traces(T') then Traces$_{\text{fin}}(T) ⊆ Traces$_{\text{fin}}(T')이다.

 

반면 그 역은 성립하지 않는데,

단, T가 terminal state가 없고(모든 path가 infinite), T'가 finite한 경우에는 성립한다.

즉, T가 terminal state가 없고 T'가 finite하고 Traces$_{\text{fin}}(T) ⊆ Traces$_{\text{fin}}(T')인 경우 Traces(T) ⊆ Traces(T')이다. 이러한 조건이 걸렸을 때만 finite trace equivalence가 trace equivalence를 의미한다.

 

 

 

Liveness Property

 safety property는 원치 않는 상태로 전이하지 않는 것을 보장하고, liveness property는 원하는 상태에 도달하는 것을 보장한다. 

 

 구분하는 방법은.. safety property의 경우 finite bad prefix가 존재하지만 liveness property는 그런 것이 없기 때문에, 이것으로 safety와 liveness를 구분할 수 있다. 즉, finite bad prefix로 해당 property를 반증할 수 있다면 safety, 그렇지 않다면 liveness이다. 정의에 따라 liveness는 모든 finite word를 infinite로 확장할 수 있는데, 따라서 finite word로 반증할 수 없기 때문이다.

 

 수식으로 정의하면 다음과 같다.

 E가 AP에 대한 LT property라고 하자. 즉, E ⊆ ($2^{\text{AP}}$)$^{\omega}$일 때, AP의 finite word가 E에 속하는 infinite word로 확장할 수 있을 때 E를 liveness property라고 한다. 즉, pref(E) = ($2^{\text{AP}}$)$^{+}$라는 것이다.

 

 

Decomposition Theorem

 모든 linear time property E는 safety property와 liveness property 2개로 나뉘고, 이 둘의 intersecion은 다시 E가 된다.

 즉, 모든 linear time property를 safety property와 liveness property의 conjunction으로 표현할 수 있다는 것이다.

 둘 다를 갖춘 property가 있을까? 있긴 한데, ($2^{\text{AP}}$)$^{\omega}$만 그렇다. 나머지는 없다.

 

 

 

Fairness

LT property는 다음 4가지로 나뉜다.

• safety property + invariant
• liveness property
• safety property와 liveness property 둘 다를 만족하는 단 하나
• 나머지의 모든 property p는 safety property와 liveness property의 교집합이다.

 

 즉, fairness assumption은 LT property가 아니다!

 

 예를 들어 [모든 process가 critical section에 들어간야 한다]는 liveness property를 생각해보자. 이를 만족하지 않는 path가 존재한다. 이처럼 liveness property는 종종 violated된다. 이는 path가 fair하지 않기 때문이다.

 이를 해결하기 위해 때문에 not fair한 몇몇 move를 없애 liveness property를 만족하게 만들 것이다.

 

 

 process fairness는 interleaving과 contention으로 인한 non-determinism의 적당한 해결책이 있다는 것을 가정한다. 이 중 대표적인 것은 아래 3가지가 있다. 유의점은, fairness property는 not fair한 action을 배제하는 것이기 때문에 어떤 것이 not fair한지 정의하는 것이 중요하다.

• unconditional fairness : 모든 process가 infinitely often하게 자신의 차례를 가져오는 것을 말한다.
• strong fairness : enabled infinitely often한 모든 process가 infinitely often하게 자신의 차례를 가져오는 것을 말한다.
• weak fairness : 특정 시간부터 continuously enable한 모든 process가 infinitely often하게 자신의 차례를 가져오는 것을 말한다.
  • enabled infinitely often : 해당 action이 수행될 수 있는 finite한 구간이 있다는 것 + process가 실행되지 않는 finite 구간이 있을 수도 있음.
  • continuously enable : 특정 구간에 해당 action이가 실행되는 구간이 연속적으로 있다는 것. 해당 process가 수행되지 않는 구간이 finitely often하게 존재한다는 뜻이다.
  • 대충 이 둘의 차이는, 구간 내에 action을 수행할 수 있는 곳이 continuous하냐, 아니면 sparse하냐로 받아들이면 될 것 같다.

 

 수식으로 정의하면 다음과 같다.

 transition system T의 action set Act에 대해 A ⊆ Act이고 $\rho$ = s$_0$ $\overrightarrow{\alpha_0}$ s$_1$  $\overrightarrow{\alpha_1}$ s$_2$ $\overrightarrow{\alpha_2}$ ... 인 infinite execution fragment $\rho$를 보자. 이 때  fairness는 action에 의해 parameterized된다.

fairness의 정의

• $\rho$는 unconditional A fairness : A에 속하는 action이 infinitely many하게 존재한다는 뜻이다.
• $\rho$는 strongly A fairness : s$_j$에서 수행할 수 있는 action이 infinetly many하게 A에 존재할 경우, 그러한 action $\alpha_i$ ∈ A가 infinetly many하게 존재한다는 뜻이다.
• $\rho$는 weak A fairness : 어떤 s$_j$에서 수행할 수 있는 action이 A에 존재할 경우, 그러한 action $\alpha_i$ ∈ A가 infinetly many하게 존재한다는 뜻이다.

 사용된 notation은 다음과 같다. Act(s$_i$)를 s$_i$에서 택할 수 있는 모든 action set이라고 하자. 각각의 의미는 다음과 같다.

• $\overset{∞}{\exists}$가 `infinitely many하게 존재함`
• $\overset{∞}{\forall}$를 `거의 모든 for all`

 

if unconditionally A-fair then strongly A-fair이고, unconditionally A-fair then weakly A-fair이다.

 

Hierarchy

 fairness assumption의 목적은 unfair execution을 삭제하는 것이 목적이다. 이 때 T의 모든 unconditional A-fair execution action ⊆ T의 모든 strong A-fair execution action ⊆ T의 모든 weakly A-fair execution action ⊆ T의 모든 가능한 execution와 같이 계층구조가 이루어져 있다.

 

 

F-fair

 fairness assumption A에 여러 개의 action을 넣는다고 해서 그 action들에 대해 fair해지는 것이 아니다. fairness의 정의는 A의 어떤 action을 infinitely often하게 수행하는 것이기 때문이다. 따라서 Fairness Assumption F는 (F$_\text{ucond}$, F$_\text{strong}$, F$_\text{weak}$)로 정의한다.

• F$_\text{ucond}$, F$_\text{strong}$, F$_\text{weak}$ ⊆ 2$^{\text{Act}}$이다.

 F$_\text{ucond}$ ⊆ F$_\text{strong}$ ⊆ F$_\text{weak}$이기 때문에 계층적으로 나눠 fairness assumption을 정의할 수 있다.

 

 그러면 F-fair를 정의하자. execution $\rho$는 F-fair iff

• 모든 A ∈ F$_\text{ucond}$일 때 unconditionally A-fair
• 모든 A ∈ F$_\text{strong}$일 때 strongly A-fair
• 모든 A ∈ F$_\text{weak}$일 때 weakly A-fair

 

FairTrace

 FairTraces$_F$(T)를  {$\rho$가 T의 F-fair execution일 때 trace($\rho$)}로 정의한다.

 

Fairness와 Safety는 irrelevant

 transition system T와, AP에 대한 LT property E가 있을 때 T $\models_F$ E $\Leftrightarrow$ FairTraces$_F$(T) ⊆ E. 즉, fairness는 safety의 역할을 할 수 없다.

 위 수식이 의미하는 것은 fairness assumption F와 LT property E를 만족하는 것과, T의 FairTraces가 E에 속한다는 것은 동치라는 뜻이다.

 

Fairness 만들기

 fairness assumption은 가능한 한 weak해야 한다. 처음에는 weak로 잡고, 안 되면 strong으로, 안 되면 uncondition으로 fairness assumption을 옮겨야 한다.

 

 

Fairness와 Safety의 관계

 fairness assumption은 safety property에 영향을 주지 않는다. 단 이를 위해서는 몇 가지 스킬을 써야 한다.

 

 realizability는 각각의 initial finite path fragment가 F-fair path로 확장되어야 한다는 것을 요구한다.

 realizable의 정의는 fairness assumption는 T의 reachable한 state s에 대해, s에서 시작하는 F-fair path가 존재하는 경우 transition system T에서 realizable하다고 한다.

 

 이 때 realizable fairness assumption은 safety property와 관계없다. 만약 transition system T와 safety property E에 대해 fairness assumption F가 realizable 하다면 T $\models$ E iff T $\models_F$ E이다.

 위 명제는 non-realizable fairness assumption에 대해서는 성립하지 않는다.