크립키 구조

"오늘의AI위키"는 AI 기술로 일관성 있고 체계적인 최신 지식을 제공하는 혁신 플랫폼입니다.
"오늘의AI위키"의 AI를 통해 더욱 풍부하고 폭넓은 지식 경험을 누리세요.

1. 개요

크립키 구조는 4-튜플 M = (S, I, R, L)로 정의되며, 상태 집합, 초기 상태 집합, 상태 전이 관계, 라벨 함수로 구성된다. 명제 논리의 원자 명제 집합 AP를 사용하여 각 상태에서 유효한 원자 명제의 집합을 정의한다. 크립키 구조는 무한 경로를 구성하며, 데드락 상태는 자신에게 다시 연결되는 에지로 모델링된다. 크립키 구조는 모델 검증 분야에서 널리 사용되며, 전이 시스템과 상태 그래프의 개념과 관련이 있다.

크립키 구조

📚 더 읽어볼만한 페이지

시간 논리 - 계산 트리 논리
계산 트리 논리(CTL)는 에드먼드 M. 클라크와 E. 앨런 에머슨이 제안한 논리 체계로, 논리 연산자, 경로 연산자(A, E), 상태 연산자(X, G, F, U, W)를 조합하여 시스템 상태 변화를 기술하며 모델 검사에서 효율적인 계산이 가능하다.
시간 논리 - 선형 시제 논리
선형 시제 논리(LTL)는 미래에 대한 진술을 표현하기 위해 시간 양상 연산자를 사용하여 시스템의 속성을 명세하고 검증하는 데 활용되는 시제 논리의 한 유형이다.

1. 개요
2. 정의
- 2.1. 크립키 구조와 다른 개념과의 관계
3. 예시

2. 정의

크립키 구조는 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)

$M$ 의 경로는 각 $i > 0$ 에 대해 $R(s_i, s_{i+1})$ 가 참인 상태의 시퀀스 $\rho = s_1, s_2, s_3, ...$ 이다. 경로 $\rho$ 에 대한 단어는 원자 명제 집합의 시퀀스 $w = L(s_1), L(s_2), L(s_3), ...$ 이며, 이는 알파벳 $2^{AP}$ 에 대한 ω-단어이다.

2.1. 크립키 구조와 다른 개념과의 관계

Clarke^영어 등은 변수, 상수 및 술어 기호로 구성된 명제 논리의 원자 명제 집합인 에 대한 크립키 구조를 정의한다. 크립키 구조는 4-튜플 로 구성된다.

* : 유한 집합의 상태
* : 초기 상태 집합
* : 왼쪽 전체 관계인 전이 관계. 즉, 와 같이 이다.
* : 레이블링(또는 "해석") 함수

은 왼쪽 전체 관계이므로, 크립키 구조를 통해 무한 경로를 구성하는 것이 항상 가능하다. 데드락 상태는 자신에게 다시 연결되는 단일 발신 에지로 모델링할 수 있다. 레이블링 함수 은 각 상태 에 대해 에서 유효한 모든 원자 명제의 집합 를 정의한다.

이러한 정의에 따르면 크립키 구조는 단일 입력 알파벳을 가진 무어 머신으로 식별될 수 있으며, 출력 함수는 해당 레이블링 함수이다.

모델 검증 분야에서 이 용어가 널리 사용되지만, 일부 모델 검증 교재에서는 "크립키 구조"를 확장된 방식으로 정의하지 않거나, 아예 정의하지 않고 (라벨이 지정된) 전이 시스템의 개념을 사용한다. 이 경우 전이 시스템은 라는 동작 집합을 추가로 가지며, 전이 관계는 의 부분 집합으로 정의된다. 또한 원자 명제 집합과 상태의 라벨링 함수(위에 정의된 )를 포함하도록 확장한다. 이 접근 방식에서 동작 라벨을 추상화하여 얻은 이진 관계를 상태 그래프라고 부른다.

모달 μ-미적분의 의미론을 정의할 때, 클라크(Clarke) 등은 크립키 구조를 (하나가 아닌) 전이 집합으로 재정의하는데, 이는 위에 언급된 라벨이 지정된 전이와 동일하다.

3. 예시

원자 명제 집합을 AP^영어=p^영어, q^영어로 둔다. p^영어와 q^영어는 크립키 구조가 모델링하는 시스템의 임의의 부울 속성을 모델링할 수 있다.

오른쪽 그림은 크립키 구조 M^영어=(S^영어, I^영어, R^영어, L^영어)를 보여주는데, 여기서
* S^영어={s₁, s₂, s₃}이다.
* I^영어={s₁}이다.
* R^영어={(s₁, s₂), (s₂, s₁) (s₂, s₃), (s₃, s₃)}이다.
* L^영어={(s₁, {p, q}), (s₂, {q}), (s₃, {p})}이다.

M^영어은 경로 ρ^영어=s₁, s₂, s₁, s₂, s₃, s₃, s₃, ...를 생성할 수 있으며, w^영어={p, q}, {q}, {p, q}, {q}, {p}, {p}, {p}, ...는 경로 ρ^영어에 대한 실행 워드이다.
M^영어은 언어 ({p, q}{q})*({p})^ω ∪ ({p, q}{q})^ω에 속하는 실행 워드를 생성할 수 있다.