주 메뉴 열기

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

정의편집

크립키 구조는[1] 4-튜플   로 기술되며, 각 기호의 의미는 다음과 같다.

  •   : 유한한 상태들로 구성된 집합
  •   : 초기 상태의 집합
  •   : 상태 전이 ( )
  •   : 라벨 함수, AP 는 단위 명제(atomic proposition)

참고 및 각주편집

  1. Clarke, Grumberg and Peled: "Model Checking", page 14. The MIT Press, 2000.