크립키 구조 문서 원본 보기

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

== 정의 ==

크립키 구조는<ref>Clarke, Grumberg and Peled: "Model Checking", page 14. The MIT Press, 2000.</ref> [[n-튜플|4-튜플]] <math>M = (S,\; I,\; R,\; L)</math> 로 기술되며, 각 기호의 의미는 다음과 같다.

* <math>S\;</math> : 유한한 상태들로 구성된 집합

* <math>I \subseteq S</math> : 초기 상태의 집합

* <math>(s,s') \in R \subseteq S \! \times \! S \;</math> : 상태 전이 (<math>\; \forall s \! \in \! S, \; \exists s' \!\! \in \! S</math>)

* <math>L: S \rightarrow 2^{AP}</math> : 라벨 함수, AP는 단위 명제(atomic proposition)

== 같이 보기 ==
* [[시간 논리]]
* [[선형 시제 논리]]
* [[계산 트리 논리]]

== 각주 ==
{{각주}}

{{토막글|컴퓨터 과학}}

[[분류:시간 논리]]