승인되는 길이 있으면, 모든 신청이 끝내 승인될까요?

여기서는 신청 한 건이 어느 단계에 있는지를 상태로 삼겠습니다. s0는 접수 전, s1은 신청 접수, s2는 담당 확인, s3은 승인 완료입니다. 오류도 검사할 수 있도록 s4를 승인 없이 대출이 진행된 상태로 넣습니다. 뒤에서 오류로 가는 이동을 추가하기 전까지 s4에는 접수 전 상태에서 닿을 수 없습니다. 상태 목록에 있다는 것과 실제 시작점에서 도달할 수 있다는 것은 따로 확인합니다.

상태에 붙일 짧은 사실 표시도 두 개 정하겠습니다. g는 “승인 완료”를 뜻하므로 s3에서만 참입니다. bad는 “승인 전 대출 오류”를 뜻하므로 s4에서만 참입니다. 나머지 상태에서는 두 표시가 모두 거짓입니다. 이제 승인에 이르는지를 물을 때마다 긴 문장을 반복하지 않고 g를 사용할 수 있습니다.

상태는 이 검사를 위해 필요한 정보를 정리한 모형의 한 칸입니다. 대출자의 이름, 책의 종류, 서버의 실제 시각은 이 모형에 없습니다. 그런 정보가 승인 절차를 바꾼다면 상태나 이동을 더 세분해야 합니다. 지금 얻을 결론은 정해 둔 다섯 상태와 그 이동에 관한 결론입니다.

맞습니다. 기본 절차에서는 s0 다음에 s1로 가고, s1 다음에는 s2로 갑니다. s2에서 선택이 갈립니다. 재검토하면 s1로 돌아가고, 승인하면 s3으로 갑니다. s2→s1과 s2→s3을 함께 적어야 두 선택이 모두 계산에 들어갑니다. 각 화살표는 허용되는 바로 다음 이동 하나를 뜻합니다. 화살표가 있다는 사실만으로 그 이동을 반드시 선택한다고 정하지는 않습니다.

원전은 모든 상태에 적어도 하나의 다음 상태가 있는 관계를 사용합니다. 이 조건을 맞추기 위해 s3과 s4에는 각각 자기 자신으로 가는 선을 둡니다. 승인 완료 뒤에는 “완료된 상태가 계속 유지된다”고, 오류 뒤에는 “오류가 발생한 상태가 계속 유지된다”고 기록하는 약속입니다. 한 건의 절차를 마친 뒤 새 신청을 받는 동작은 이번 모형에서 다루지 않습니다.

이 약속 덕분에 모든 실행을 끝없이 이어지는 상태 열로 읽을 수 있습니다. s3의 자기루프를 실제 승인 업무를 무한히 반복한다는 뜻으로 읽을 필요는 없습니다. 반면 s1과 s2 사이의 왕복은 승인 전에 재검토가 계속될 수 있다는 절차의 선택을 나타냅니다. 두 종류의 반복은 이 사례에서 역할이 다릅니다.

한 경로에서 같은 상태를 여러 번 방문할 수 있기 때문입니다. s0,s1,s2,s3,s3,…은 한 경로이고, s0,s1,s2,s1,s2,s3,s3,…은 재검토를 한 번 더 한 경로입니다. 재검토를 두 번, 세 번 하고 승인하는 경로도 있습니다. 그뿐 아니라 s0,s1,s2,s1,s2,…처럼 승인을 영원히 미루는 경로도 이동표에 맞습니다.

CTL은 이런 갈래를 구별해서 말하는 시간논리입니다. E는 현재 상태에서 시작하는 경로가 적어도 하나 있다는 뜻이고, A는 그 상태에서 시작하는 모든 경로를 살핀다는 뜻입니다. F는 현재 또는 나중의 어느 지점, G는 현재부터 이어지는 모든 지점을 말합니다. 이들을 짝지은 EF g와 AF g는 각각 “어떤 경로에서 언젠가 승인”과 “모든 경로에서 언젠가 승인”을 뜻합니다.

“언젠가”에는 현재도 들어갑니다. 시작 상태가 이미 s3이라면 g가 지금 참이므로 EF g와 AF g가 모두 참입니다. 또한 여기서 “나중”은 상태 이동의 순서를 말합니다. 몇 초 이내에 승인되는지, 승인될 확률이 얼마인지는 이 기호와 모형에 들어 있지 않습니다.

시작점을 s0로 두면 그렇습니다. EF g가 참이라는 근거는 s0→s1→s2→s3입니다. 이 유한한 앞부분 뒤에 s3의 자기루프를 이어 붙이면 완전한 무한 경로가 됩니다. 그 경로는 네 번째 상태에서 g를 만나므로 “그런 경로가 적어도 하나 있다”는 요구를 충족합니다.

AF g는 모든 경로에서 승인을 만나야 합니다. 그런데 s0→s1로 들어간 뒤 s1→s2→s1을 계속 반복하는 경로가 있습니다. 이 경로의 어느 지점도 s3이 아니므로 g를 만나지 않습니다. 이 한 경로 때문에 s0에서 AF g가 거짓입니다. 승인 경로의 존재와 승인 없는 무한 경로의 존재가 이 모형에서 함께 성립합니다.

재검토 선 s2→s1을 지우면 상황이 달라집니다. s2의 다음 상태가 s3 하나로 줄어들어 s0에서 시작한 경로는 s1,s2,s3을 지나야 합니다. 아래 실험에서 같은 사실 표시를 유지한 채 이 선만 바꿔 보세요. 시작점을 s3이나 s4로 옮기면 이미 승인된 경우와 오류에서 벗어나지 못하는 경우도 확인할 수 있습니다.

목표에서 거꾸로 표시하면 됩니다. 처음에는 g가 지금 참인 s3만 표시합니다. 다음에는 이미 표시한 상태로 한 번에 갈 수 있는 상태를 추가합니다. “갈 수 있는 다음 상태가 하나라도 있다”가 EF 계산의 조건입니다. s2는 s3으로 갈 수 있으므로 붙습니다. s2의 다른 선택인 s1이 아직 표시되지 않았어도 괜찮습니다.

한 단계에서는 직전 단계의 표시만 사용하겠습니다. 0단계는 {s3}, 1단계는 {s2,s3}, 2단계는 {s1,s2,s3}, 3단계는 {s0,s1,s2,s3}입니다. 다음에 다시 계산해도 새 상태가 붙지 않습니다. s4에서는 s4로만 가므로 목표에 도달할 근거를 얻지 못합니다.

목표 집합을 G라고 하고, X의 상태로 가는 후속이 하나라도 있는 상태들의 집합을 Pre∃(X)라고 쓰면, 갱신 규칙은 G∪Pre∃(X)입니다. 목표에서 출발해 표시를 늘리다가 더는 바뀌지 않은 집합이 EF g의 최소고정점입니다. “고정점”은 같은 규칙을 한 번 더 적용해도 그대로인 집합, “최소”는 목표에서 이 규칙으로 얻을 수 있는 가장 작은 고정된 해라는 뜻입니다.

AF는 추가 조건을 바꿉니다. s3을 먼저 표시한 뒤, 어떤 상태의 바로 다음 상태가 모두 표시되어 있을 때 그 상태를 추가합니다. 어느 후속을 선택해도 승인에 이른다는 근거가 있어야 하기 때문입니다. s2의 후속은 s1과 s3입니다. s3은 표시되었지만 s1은 표시되지 않았으므로 s2를 추가할 수 없습니다.

s1도 후속 s2가 표시되지 않았으므로 추가할 수 없습니다. s0의 후속 s1도, s4의 후속 s4도 같은 이유로 조건을 충족하지 못합니다. 따라서 {s3}에서 한 번 계산한 결과가 다시 {s3}입니다. EF의 표시 집합은 네 상태로 자랐지만 AF의 표시 집합은 하나에서 멈춥니다.

“s1이 언젠가 승인되니 s2도 승인된다”, “s2가 언젠가 승인되니 s1도 승인된다”고 서로를 근거로 삼으면 순환만 남습니다. 실제로 {s0,s1,s2,s3}도 AF 갱신식 G∪Pre∀(X)에 넣으면 그대로 돌아오는 집합입니다. 그러나 그 큰 집합은 목표에서 출발한 단계별 근거로 얻어지지 않습니다. AF에는 목표까지의 도달 근거를 쌓아 얻는 최소고정점이 필요합니다.

이제 s2의 후속은 s3 하나입니다. 시작 집합 {s3}에서 s2를 추가할 수 있습니다. 다음 단계에는 s1의 유일한 후속 s2가 이미 표시되므로 s1을, 그다음에는 s0의 유일한 후속 s1이 표시되므로 s0를 추가합니다. 결과는 {s0,s1,s2,s3}입니다. 오류 상태 s4에는 여전히 g가 없고 자기루프만 있으므로 포함되지 않습니다.

붙은 단계 수를 상태 옆에 적어 보겠습니다. s3은 0, s2는 1, s1은 2, s0는 3입니다. 승인을 아직 만나지 않은 상태에서 한 걸음 움직일 때마다 이 수가 작아집니다. 3에서 출발해 계속 작아지는 음이 아닌 정수는 끝없이 내려갈 수 없습니다. 이 모형에서는 s0에서 최대 세 번 이동하면 g를 만나야 한다는 구체적인 근거가 됩니다.

계산 자체도 끝납니다. 표시를 지우지 않고 유한한 다섯 상태 중에서 새 상태만 추가하기 때문입니다. 다만 계산이 끝난다는 것과 시스템의 모든 실행이 승인된다는 것은 다른 진술입니다. 재검토 선이 있는 모형에서도 AF 계산은 곧 끝나지만 결과 집합에 s0가 없습니다. 계산은 완료 여부의 참과 거짓을 모두 판정합니다.

유한한 앞부분과 반복할 구간을 주면 충분합니다. 기본 모형에서 s0→s1이 앞부분이고, s1→s2→s1이 반복 구간입니다. 앞부분으로 반복 구간에 들어간 뒤 그 구간을 계속 돌면 승인 없는 무한 경로 하나가 정해집니다. 각 선이 이동표에 있는지, 앞부분과 반복 구간 어느 곳에도 s3이 없는지 확인하면 됩니다.

단지 “아직 승인되지 않은 열 단계”를 출력하는 것보다 이 근거가 강합니다. 열한 번째 단계에 승인될 수도 있으므로 유한한 지연 기록만으로 AF를 반박할 수는 없습니다. 반면 같은 승인 없는 구간으로 되돌아오는 선이 있으면 그 선택을 계속 반복할 수 있습니다. 이 모형은 반복 횟수의 제한이나 공정성 조건을 추가하지 않았습니다.

유한 그래프의 승인 없는 무한 경로는 결국 어떤 상태를 다시 방문합니다. 그 경로에서 반복된 상태 사이를 떼어 내면 승인 없는 순환을 얻습니다. 따라서 이 실험은 s3을 제외하고 도달 가능한 순환을 찾습니다. 발견하면 그곳까지의 진입길과 순환을 함께 보여 줍니다. 시작점이 이미 s3이면 현재 g가 성립하므로 이런 AF 반례는 없습니다.

그렇습니다. “승인 전 대출 오류가 한 번도 생기지 않는다”는 요구를 AG ¬bad로 적겠습니다. ¬bad는 해당 상태가 오류 상태가 아니라는 뜻이고, AG는 모든 경로의 모든 지점에서 그 조건을 확인합니다. 기본 모형의 s0에서는 s4로 가는 선이 없으므로 AG ¬bad가 참입니다. 재검토가 끝없이 이어져도 오류 상태를 만나지 않는 한 이 안전 조건은 유지됩니다.

이제 s1→s4라는 잘못된 지름길을 하나 추가합시다. s0→s1→s4를 따라가면 세 번째 상태에서 bad가 참입니다. 모든 경로가 안전해야 한다는 요구는 이 한 경로로 깨집니다. 안전 실패를 설명할 때는 오류에 도착하는 유한한 앞부분만 있으면 충분합니다. AF 실패에서 목표를 영원히 피한다는 반복 근거가 필요했던 경우와 구별됩니다.

계산은 오류에서 거꾸로 진행할 수 있습니다. EF bad가 참인 상태는 오류에 도달할 수 있는 상태입니다. 그 집합의 바깥이 AG ¬bad가 참인 상태입니다. 원전도 AG 형태의 요구가 실패하면 잘못된 상태로 가는 경로를 보여 주는 기능을 설명합니다. 아래 실험은 같은 원리를 이 다섯 상태에 적용해 실제 반례 경로를 구합니다.

표의 세 설계를 s0에서 비교해 보겠습니다. 첫째는 기본 설계입니다. 승인 경로가 있으므로 EF g는 참, 재검토가 끝없이 가능하므로 AF g는 거짓, 오류에 닿지 못하므로 AG ¬bad는 참입니다. 둘째는 재검토 선을 지운 설계입니다. s0에서 승인까지 가는 선택만 남아 세 요구가 모두 참입니다.

셋째에서는 재검토 선을 지운 상태로 오류 지름길 s1→s4를 넣습니다. 승인 경로 s0→s1→s2→s3은 남아 있으므로 EF g는 여전히 참입니다. 동시에 s0→s1→s4→s4→…도 허용됩니다. 이 경로는 오류를 만나고 승인을 영원히 만나지 않으므로 AG ¬bad와 AF g가 모두 거짓이 됩니다.

이 비교에서는 상태별 사실 표시를 그대로 두고 선만 바꿨습니다. 가능한 선을 추가하면 기존의 성공 경로가 사라지지는 않지만, 모든 경로에 요구한 조건을 깨는 새 경로가 생길 수 있습니다. 따라서 수정 뒤에는 필요한 요구를 각각 다시 검사해야 합니다. 승인 가능성 하나가 안전과 완료 보장까지 대신해 주지는 않습니다.

그런 제외에는 어떤 선택을 반드시 보장하는지 명시한 가정이 필요합니다. 원전은 공정성 조건을 둔 CTLF도 다룹니다. 그때에는 모든 가능한 경로 중에서 공정성 조건을 충족하는 경로만 양화의 대상으로 삼습니다. 논문이 기본적으로 다루는 형태는 지정한 상태 조건들 각각이 경로에서 무한히 자주 성립하도록 요구하는 방식입니다.

이 승인기에서 “언젠가 승인이 나올 것”이라고 가정하고 승인 없는 경로를 빼면 완료 요구를 만족시키기 쉬워집니다. 그러나 그 가정 자체를 시스템이나 운영 규칙이 보장하는지는 별도의 문제입니다. 실제로 보장하지 않은 기대를 넣으면, 검사에서 제외한 바로 그 경로가 운영 중에 나타날 수 있습니다. 이 편의 세 실험에는 공정성 제한을 넣지 않았습니다. 이동표에 맞는 모든 무한 경로를 그대로 셉니다.

재검토 선을 지우는 것과 공정성 조건으로 어떤 무한 경로를 제외하는 것도 구별해야 합니다. 선을 지우면 재검토 한 번도 허용되지 않습니다. 공정성 조건은 유한 횟수의 재검토를 허용하면서 끝없이 재검토만 하는 진행을 제외할 수 있습니다. 어느 쪽을 선택하든 바뀐 절차나 경로 가정을 드러낸 뒤 그 범위에서 결과를 읽어야 합니다.

상태 집합과 이동 관계가 유한하고 완전히 주어졌기 때문입니다. EF는 목표로 닿을 수 있는 상태를 거꾸로 모두 모읍니다. AF는 모든 후속에서 목표까지의 근거를 얻는 상태를 모읍니다. AF에서 남은 실패는 목표를 피하며 되풀이할 수 있는 순환으로 설명할 수 있습니다. 실행을 일정 횟수까지만 시험하고 멈춘 결과와 달리, 계산은 같은 상태로 돌아왔을 때 다시 가능해지는 선택까지 이용합니다.

원전의 정리 3.1은 CTL 식의 길이를 |f|, 상태 수를 |S|, 이동선 수를 |R|이라고 할 때 O(|f|·(|S|+|R|)) 시간에 검사할 수 있는 알고리즘을 제시합니다. 식을 이루는 작은 부분부터 참인 상태를 표시하고, 그래프 탐색을 알맞게 구성해 얻는 경계입니다. 이것은 원전에 주어진 입력 모형 크기에 대한 이론적 계산량입니다.

이 페이지의 실험은 표시가 늘어나는 과정을 보여 주려고 상태 전체를 여러 차례 훑는 간단한 집합 반복을 사용합니다. 따라서 실험 코드에 원전의 최적 시간 경계를 그대로 붙이지 않습니다. 또한 이 도구는 고정된 다섯 상태에서 EF g, AF g, AG ¬bad를 검사합니다. 임의의 프로그램을 입력받아 모든 요구를 검증하는 범용 도구로 구현한 것은 아닙니다.

유한하다는 것만으로 작다는 보장은 없습니다. 예를 들어 각각 세 상태를 갖는 구성 요소 네 개를 함께 기록하면, 조합의 후보는 3×3×3×3=81개입니다. 구성 요소가 여덟 개이면 3⁸=6,561개가 됩니다. 실제로 도달할 수 없는 조합을 제거할 수 있어도 전체 상태가 빠르게 늘어날 수 있습니다. 원전도 구성 요소들의 상태를 합친 전역 상태 그래프가 곱의 크기로 커질 수 있음을 설명합니다.

상태 수를 줄일 때에는 무엇을 생략해도 해당 요구의 판단을 보존하는지 따져야 합니다. 이 승인기에 별도의 취소 요청, 서버 고장, 승인 철회 기능을 넣으면 새 상태와 이동이 필요할 수 있습니다. 그것들이 실제 시스템에 존재하는데 모형에서 빼면, 이 모형의 AG ¬bad가 참이어도 실제의 모든 오류가 없다고 결론 내릴 근거는 부족합니다.

실무의 검증에서는 명세 문장이 원하는 요구를 정확히 적었는지, 모형이 관련된 동작을 충분히 담았는지, 검사기가 그 모형을 올바르게 계산했는지를 함께 확인해야 합니다. 오늘의 작은 예는 마지막 계산을 끝까지 드러내는 데 초점을 맞춥니다. 앞의 두 준비도 결과의 적용 범위를 결정합니다.

기본 모형의 시작 상태 s0에서 승인에 이르는 경로는 있습니다. EF g가 참이며, s0→s1→s2→s3이 근거입니다. 그러나 모든 경로가 승인에 이르는 것은 아닙니다. AF g는 거짓이고, s1과 s2 사이의 반복이 반례입니다. 동시에 오류 상태 s4로 가는 경로는 없으므로 AG ¬bad는 참입니다. 이 세 결과를 함께 적으면 승인 가능성, 완료 보장, 오류 방지를 구체적으로 나누어 설명할 수 있습니다.

재검토 선을 지우고 오류 지름길도 두지 않으면 s0에서 세 요구가 모두 참입니다. 여기에 오류 지름길을 추가하면 승인 가능성은 남지만 완료 보장과 오류 방지가 깨집니다. 어느 결과든 상태 목록, 사실 표시, 이동 관계, 시작점, 공정성 가정을 함께 적어야 재현할 수 있습니다. 조건이 달라지면 이전의 판정을 그대로 옮길 수 없습니다.

이 논문의 핵심 기여를 따라 우리가 배운 것은 요구 문장을 유한한 모형에 적용해 체계적으로 판정하는 방법입니다. 기호를 붙인 뒤에도 “어느 경로를 말하는가”, “어느 상태에서 참인가”, “실패를 보여 주는 자료가 무엇인가”를 끝까지 확인합니다. 한 번 성공했다는 기록에서 출발한 질문이, 가능한 모든 진행에 관한 검증 가능한 질문으로 바뀐 것입니다.