fairness constraints

좋습니다. 아래는 Fairness Constraints가 적용된 Kripke 구조 예시입니다. 복사하기 쉬운 텍스트 형식으로 제공하겠습니다.


---

Kripke 구조

S   = {s0, s1, s2}
S₀  = {s0}
R   = {
         (s0, s1),
         (s1, s1),  // s1에서 무한히 머무를 수 있음
         (s1, s2)
     }
AP  = {ready, run, done}
L(s0) = {ready}
L(s1) = {ready}
L(s2) = {run, done}


---

공정성 제약 (Fairness Constraint)

Justice (weak fairness):

if ready holds infinitely often,
then run must also happen infinitely often

형식적으로:

Justice constraint: G F ready → G F run

이 의미는 다음과 같습니다:

어떤 실행 경로에서 ready가 무한히 자주 등장하면,

그 경로에서는 run도 무한히 자주 등장해야 함.



---

의도된 의미

이 시스템에서는:

s1에서 계속 ready 상태로 머물 수 있음 (s1 → s1 무한 반복 가능)

하지만 s2로 전이하면 run이 발생


공정성 제약이 없다면:

(s0 → s1 → s1 → s1 → ...) 같은 경로가 유효함 → run이 절대 발생하지 않음
→ 비현실적이지만 CTL 식 EF run은 거짓으로 판단됨


공정성 제약을 추가하면:

무한히 ready한데 run이 한 번도 안 나오면 그 경로는 비공정
→ 검사에서 제외됨
→ EF run은 공정한 경로 내에서는 참



---

필요하시면 이 예시를 그림이나 그래프로 시각화해 드릴 수도 있습니다.