Kripke 구조 예시

Kripke 구조 M = (S, S₀, R, AP, L)

S   = {s0, s1, s2}
S₀  = {s0}
R   = {(s0, s1), (s1, s1), (s1, s2)}
AP  = {start, processing, done}
L(s0) = {start}
L(s1) = {processing}
L(s2) = {done}

이 구조는 다음과 같은 시스템을 나타냅니다:

시작 상태는 s0이며, start 상태이다.

s0에서 s1로 전이된다.

s1은 processing 상태이고, 자기 자신으로 루프 가능.

s1에서 s2로 갈 수 있으며, s2는 done 상태이다.



---

사용 예 (CTL 식 평가)

EF done:
s0에서 출발해 어떤 경로를 따라가면 언젠가 done 상태(s2)에 도달할 수 있다 → 참

AG ¬done:
모든 경로에서 done에 도달하지 않아야 한다 → 거짓 (s2에서 done이 참이므로)