state formula와 path formula의 공통점과 차이점

공통점:

둘 다 **시계열 논리(temporal logic)**의 논리식이다.

둘 다 시스템의 동작을 형식적으로 기술하는 데 사용된다.

둘 다 Model Checking에서 사용되며, 시스템 모델이 이 식을 만족하는지 검사하는 대상이다.



---

차이점:

State formula

→ “지금 이 상태에서 어떤 조건이 참인가?”를 묻는 식
→ 하나의 상태만 보고 판단


지금 상태가 error가 아닌가? → ¬error

지금 상태에서 모든 경로에서 p가 언젠가 참인가? → AF p

지금 상태에서 어떤 경로를 따라가면 q가 곧 참인가? → EX q


→ 현재 상태에서 이 조건이 만족되는지 바로 판단 가능


---

Path formula

→ “하나의 경로(상태들의 흐름) 위에서 어떤 일이 일어나는가?”를 묻는 식
→ 경로 전체를 보고 판단

예:

이 경로에서 다음 상태가 p인가? → X p

이 경로에서 p가 계속 유지되다가 q가 언젠가 참이 되는가? → p U q

이 경로에서 r이 항상 참인가? → G r


→ 지금 이 경로에서 전체적으로 그 일이 일어나는지를 봐야 판단 가능


---

비유로 설명:

State formula는 "이 순간(상태)에 이 조건이 맞아?"

Path formula는 "이 경로(흐름)에서는 이런 일이 일어나?"



---

CTL 기준 요약:

CTL에서는 모든 식이 state formula

E[...], A[...]로 path formula를 감싸서 state formula를 구성

CTL 자체에는 path formula가 문법상 단독으로 쓰이지 않음



---

궁금하시면 상황별 예시도 더 만들어드릴 수 있습니다.



---

요약:

Path formula는 실행 경로의 성질을 나타내며,

State formula는 "이 상태에서 어떤 경로의 성질이 만족되는가?"를 기술한다.

CTL은 path formula 위에 경로 한정자(A, E)를 붙여 만든 state formula로만 구성됨.