크립키 모델

소프트웨어 개발 과정에서 테스트와 품질 보증은 많은 시간이 드는 단계이다. 이 단계에 드는 비용과 시간을 줄이기 위해 여러 기법이 사용되는데, 그중 하나가 소프트웨어 검증이다. 모델 검사(model checking)는 크립키 모델(Kripke model)에 기반한 소프트웨어 검증 기법이다.

크립키 모델은 5-튜플 $(P, S, S_0, R, L)$로 정의된다. 여기서 $P$는 원자 명제의 유한 집합, $S$는 상태의 유한 집합, $S_0 \subset S$는 초기 상태의 집합, $R \subset S \times S$는 전이 관계, $L \subset S \times P$는 진리 관계이다. 이 문제에서는 초기 상태를 고려하지 않으며, $R$는 반사적(reflexive) 관계이므로 모든 상태 $s \in S$에 대해 $R(s, s)$가 성립한다.

상태 $s$에서 시작하는 경로(path) $\pi$는 $s_0 = s$이고 모든 $i \ge 0$에 대해 $(s_i, s_{i+1}) \in R$을 만족하는 무한 상태 수열 $s_0 s_1 \ldots$이다.

시간 논리(temporal logic)와 그 부분집합인 계산 트리 논리(CTL)는 시간에 관한 명제를 기술한다. 크립키 모델은 CTL로 기술된 성질을 검사하는 데 자주 쓰인다.

CTL의 논리식에는 상태 논리식과 경로 논리식 두 종류가 있으며, 각각 상태와 경로에 대해 값이 평가된다.

$p \in P$이면 $p$는 상태 논리식이며, $(s, p) \in L$일 때에만 상태 $s$에서 성립한다.

$f$가 경로 논리식이면 $\mathrm{\mathbf{A}} f$와 $\mathrm{\mathbf{E}} f$는 상태 논리식이다. 여기서 $\mathrm{\mathbf{A}}$와 $\mathrm{\mathbf{E}}$는 경로 한정사이다:

• $\mathrm{\mathbf{A}} f$는 상태 $s$에서 시작하는 모든 경로에 대해 $f$가 성립할 때에만 $s$에서 성립한다;
• $\mathrm{\mathbf{E}} f$는 상태 $s$에서 시작하며 $f$가 성립하는 경로 $\pi$가 하나라도 존재할 때 $s$에서 성립한다.

$f$와 $g$가 상태 논리식이면 $\mathrm{\mathbf{G}} f$와 $f \mathrm{\mathbf{U}} g$는 경로 논리식이다. 여기서 $\mathrm{\mathbf{G}}$와 $\mathrm{\mathbf{U}}$는 시간 연산자이다:

• $\mathrm{\mathbf{G}} f$ (Globally)는 경로 $\pi = s_0 s_1 \ldots$의 모든 $i \ge 0$에서 상태 $s_i$에 대해 $f$가 성립할 때에만 그 경로에서 성립한다;
• $f \mathrm{\mathbf{U}} g$ (Until)는 경로 $\pi = s_0 s_1 \ldots$에서, 상태 $s_i$에서 $g$가 성립하고 그 앞의 모든 상태 $s_0, s_1, \ldots, s_{i-1}$에서 $f$가 성립하는 $i \ge 0$이 존재할 때 성립한다.

상태 논리식 $f$로 기술된 성질을 검증한다는 것은 $f$가 성립하는 모든 상태를 찾는 것을 의미한다. 임의의 성질을 검증하는 것은 꽤 복잡한 문제이다. 이 문제는 더 쉽다. 원자 명제 $x$, $y$에 대한 시간 논리식 $\mathrm{\mathbf{E}}(x \mathrm{\mathbf{U}} (\mathrm{\mathbf{A}} \mathrm{\mathbf{G}} y))$로 기술된 성질을 검증하는 프로그램을 작성하면 된다.

첫 번째 줄에는 상태의 수 $n$, 전이의 수 $m$, 원자 명제의 수 $k$가 주어진다 ($1 \le n \le 10\,000$; $0 \le m \le 100\,000$; $1 \le k \le 26$).

이어지는 $n$개의 줄은 각각 하나의 상태를 기술한다. 상태 $i$ ($1 \le i \le n$)는 그 상태에서 참인 원자 명제의 개수 $c_i$와 그 명제들의 목록(공백으로 구분)으로 주어진다 ($0 \le c_i \le k$). 원자 명제는 알파벳 소문자 처음 $k$개로 나타낸다.

다음 $m$개의 줄은 각각 하나의 전이를 기술하며, 두 정수 $s$와 $t$ ($1 \le s, t \le n$; $s \ne t$)로 이루어진다 — 상태 $s$에서 상태 $t$로의 전이이다. 모델에는 모든 상태 $s$에 대한 자기 전이 $(s, s)$가 암묵적으로 포함된다(입력에는 나열되지 않는다). 같은 전이가 두 번 나열되지는 않는다.

마지막 줄에는 검증할 성질이 주어지며, 항상 E(xU(AGy)) 형태이다. 여기서 x와 y는 원자 명제이다.

첫 번째 줄에 검증한 성질이 성립하는 상태의 개수를 출력한다. 이어지는 줄에는 그 상태들의 번호를 증가하는 순서로 출력한다.