Model Checking모델 체킹

경로 위에서의 논리. 단일 선형 시간 경로 가정.

기본 연산자:
  X φ  : 다음 상태에서 φ 성립 (neXt)
  F φ  : 미래에 언젠가 φ 성립 (Finally)
  G φ  : 항상 φ 성립 (Globally)
  φ U ψ: ψ가 성립할 때까지 φ 성립 (Until)

예:
  G (request → F response)  -- 요청은 언젠가 응답됨
  G ¬(critical₁ ∧ critical₂) -- 상호 배제
  G (F fair)                  -- 공정성

분기 시간 논리. 가능한 모든 경로 고려.

경로 한정자:
  A: 모든 경로 (All paths)
  E: 어떤 경로 (Exists path)

상태 공식:
  AX, EX, AF, EF, AG, EG, AU, EU

예:
  AG (request → AF response)   -- 모든 경로에서
  EF (success)                  -- 성공 상태 도달 가능
  AG EF restart                 -- 항상 재시작 가능

CTL 모델 체킹 (레이블링 알고리즘):
1. 부공식부터 시작해 상향식으로 레이블 부착
2. 각 상태에 성립하는 부공식 집합 계산
3. 초기 상태에 전체 공식이 레이블 되면 만족

시간 복잡도: O(|φ| × |S|)
  |φ|: 공식 길이
  |S|: 상태 수 + 전이 수

n개 프로세스가 각 m개 상태 → m^n 상태

완화 기법:
1. BDD (Binary Decision Diagram): 심볼릭 모델 체킹
2. 부분 순서 환원 (Partial Order Reduction)
3. 추상화 (Abstraction)
4. 유한 편개 (Bounded Model Checking, BMC)
   - SAT 솔버 활용
   - "깊이 k까지 반례 있는가?"