크립키 구조

크립키 구조(Kripke Structure)는 논리학자 솔 크립키가 1963년 제안한, 비결정 유한 상태 오토마타의 일종이다. 모델 검사에서 시스템의 움직임을 기술하는데 사용된다. 크립키 구조는 접근 가능한 상태(state)들을 나타내는 노드(node)와, 상태 전이(state transition)을 나타내는 엣지로 구성된 그래프의 모양이다. 여기에 각 노드에 매핑되는 라벨 함수(labelling function)이 있어, 어떤 상태에 대해 어떤 속성값들의 집합을 대응시킨다. 시간 논리의 주요 논리 구조들은 크립키 구조로 기술되고 있다.

정의

크립키 구조는 4-튜플 $M=(S,\;I,\;R,\;L)$ 로 기술되며, 각 기호의 의미는 다음과 같다.

• $S\;$ : 유한한 상태들로 구성된 집합

• $I\subseteq S$ : 초기 상태의 집합

• $(s,s')\in R\subseteq S\!\times \!S\;$ : 상태 전이 ($\;\forall s\!\in \!S,\;\exists s'\!\!\in \!S$)

• $L:S\rightarrow 2^{AP}$ : 라벨 함수, AP는 단위 명제(atomic proposition)