\[ \newcommand{\complexI}{\mathbf{i}} \newcommand{\imaginaryI}{\mathbf{i}} \newcommand{\cis}{\operatorname{cis}} \newcommand{\vecu}{\mathbf{u}} \newcommand{\vecv}{\mathbf{v}} \newcommand{\vecw}{\mathbf{w}} \newcommand{\vecx}{\mathbf{x}} \newcommand{\vecy}{\mathbf{y}} \newcommand{\vecz}{\mathbf{z}} \]
ROSÉ

시제논리: 아리스토텔레스의 해전에서 프로그램 검증까지

by Ariel Daley
written by Ariel Daley 40 views

명제논리와 일계논리를 공부하다 보면 자연스럽게 사용하는 성질이 있다. 바로 어떤 진술이든 참 또는 거짓, 둘 중 하나의 값만 매겨질 수 있다는 것이다. “2는 소수이다”는 참이고 “모든 자연수는 짝수이다”는 거짓이다. 진릿값이 하나 정해지고 나면 그것으로 끝이다. 그런데 수학 바깥으로 잠깐 나가 보자. “비가 내린다”라는 문장은 참인가? 지금은 그럴 수 있다. 한 시간 뒤에는 거짓일지도 모른다. “소크라테스는 앉아 있다”는 언제 묻느냐에 따라 답이 바뀐다. 이런 문장은 시점을 지정하지 않고서는 진릿값이 하나로 정해지지 않는다. 진릿값이 시간에 종속되기 때문이다.

시간을 따로 표현하지 않는 표준 명제논리는 이렇게 진릿값이 시간에 종속되는 진술을 표현할 수 없다. 수학에서는 그래도 괜찮다. 하지만 변하는 것을 따져야 하는 경우, 예컨대 실행되고 있는 프로그램, 미래에 대한 약속, 아직 정해지지 않은 내일에 대하여 논하려면, 표준 명제논리만으로는 부족하다.

이 글에서는 논리학자들이 시간을 다루는 논리를 어떻게 구성하였는지, 그 역사를 따라가 본다. 2300년 묵은 아리스토텔레스의 수수께끼에서 출발하여, 프라이어의 시제 연산자와 시간의 의미론을 지나, 오늘날 컴퓨터과학자들이 프로그램이 제대로 작동하는지 증명하는 데에 쓰는 언어까지 살펴볼 것이다.

시간에 종속되는 진릿값

먼저 명제논리의 한계점을 다시 살펴보자. 명제논리에서는 원자명제 \(p\)에 참 또는 거짓이 배정되고, 합성명제의 진릿값은 그 배정에 의하여 완전히 결정된다. “\(p\)가 지금은 참이지만 나중엔 거짓이 된다”와 같은 진술을 표현할 방법이 없다. 시간이라는 차원이 언어 안에 들어 있지 않은 것이다.

구체적인 문장을 사용하여 확인해 보자. “요청을 하면 언젠가 응답이 온다.”라는 문장을 살펴보자. 이 문장을 명제논리로 옮기려면 기껏해야 \(\text{request} \to \text{response}\) 정도가 된다. 그런데 이 조건문은 한 순간만을 표현한다. 어떤 시점에서 요청하는 행위가 참이면 그 시점에서 응답하는 행위가 참이라는 뜻일 뿐이다. 우리가 정작 말하려던 것은 다르다. 어느 순간에든 요청을 하면, 그 순간 또는 그 뒤의 어느 순간에 응답이 온다는 것이다. “언젠가”도 “어느 순간에든”도 모두 시간을 표현하는 양화인데, 명제논리의 언어로는 표현할 수 없다.

그렇다면 일계논리를 사용하면 이 문제가 해결될까? 시간을 객체로 끌어들이면 가능하긴 하다. 시점들의 정의역을 두고, 술어마다 시간 변수를 하나씩 더하고, 순서 관계 \( < \)와 등호를 써서 \(t\le t'\)를 \(t < t'\) 또는 \(t = t'\)인 것으로 정의하면, 위 문장은 다음과 같이 표현할 수 있다. \[ \forall t\,\big(\text{Request}(t) \to \exists t'\,(t \le t' \wedge \text{Response}(t'))\big) \] 이렇게 모든 술어에 시간 변수를 추가하여 시간을 객체로 다루는 방식을 ‘시간 인자 방법(method of temporal arguments)’이라고 부른다.

하지만 이와 같이 일계논리를 사용하여 시간을 다루는 방법은 문제가 있다. 첫째, 번거롭다. 술어마다 시간 변수를 추가하고, 시간은 명시적인 양화사로 일일이 옮겨야 하는 객체가 된다. 둘째, 시간이 객체가 되어 버린다. 우리가 현실에서 시간을 다루는 방식은 그렇지 않다. 우리는 ‘지금’이라는 순간에서 앞과 뒤를 내다보지, 모든 순간을 한 줄에 늘어놓고 변수로 가리키며 살지 않는다. 셋째, 일계논리로 시간 의존성을 표현할 수는 있지만, 모든 시간 양화를 표면으로 드러내야 해서 시제적 언어의 자연스러움을 잃는다. 위 문장을 \(\forall t\)을 사용하여 표현하면, 전체 문장은 시간과 무관하게 참, 거짓으로 하나의 진릿값을 가진다. 물론 일계논리 안에서도 열린 형식이나 시간 변수를 사용하여 시점 상대성을 표현할 수 있지만, 그 시점은 문법 밖의 ‘현재’가 아니라 명시적으로 다루는 객체가 된다.

여기서 갈림길이 생긴다. 한쪽 길은 방금 본 것처럼, 시간을 명시적인 객체로 두고 고전논리를 사용하여 표현하는 것이다. 이러한 방법으로 논리 전개를 할 수는 있지만, ‘시간 안에서 참’이라는 감각이 사라진다. 다른 길은 시간을 객체가 아니라 언어의 골격 자체에 새겨 넣는 것이다. 진릿값이 시점에 따라 달라질 수 있는 가능성을 열어두고, 시간 이동을 양화사가 아니라 전용 연산자로 표현하는 길이다. 이 두 번째 길로 들어선 사람이 아서 프라이어다.

아리스토텔레스의 해전

그 길을 더 따라가기 전에, 시간과 진릿값의 관계를 따지는 문제가 얼마나 오래된 것인지 짚고 넘어가자. 무대는 기원전 4세기, 아리스토텔레스의 『명제론』(De Interpretatione) 9장이다. 흔히 ‘내일의 해전(sea battle tomorrow)’ 논변으로 불린다.

다음과 같은 문장을 생각해 보자. “내일 해전이 일어날 것이다.” 고전논리의 이가원리에 따르면 어떤 명제든 참이거나 거짓이다. 그러니 이 문장도 지금 이미 참이거나 지금 이미 거짓이어야 하는 것처럼 보인다. 그런데 여기에 “지금 이미 참인 미래 명제는 피할 수 없다”라는 생각을 덧붙이면 문제가 생긴다. 지금 이미 참이라면 내일 해전은 피할 수 없이 일어나고, 지금 이미 거짓이라면 내일 해전은 일어나지 않을 수밖에 없다. 어느 쪽이든 미래는 이미 정해져 있는 것처럼 보인다.

아리스토텔레스는 이 결론을 받아들이고 싶지 않았다. 그가 택한 길을 두고 해석이 갈리긴 하지만, 널리 받아들여지는 해석은 이렇다. 미래의 우연한 사건을 말하는 문장은 지금 참 또는 거짓으로 확정되어 있지 않다. (이 해석을 형식화하는 방식은 갈린다. Łukasiewicz식 3치 논리(Three-valued logic)는 제3의 값을 도입하며, 이 경우 \(p\vee\neg p\)도 고전적 의미의 참으로 남지 않는다. 반면 초월진릿값 방식의 접근(supervaluationism)에서는 \(p\)와 \(\neg p\) 각각은 아직 참/거짓이 아니어도 \(p\vee\neg p\)는 참으로 둘 수 있다. 이러한 방식이 가지는 고전논리와의 차이점은 미래 우연 명제도 이미 참 또는 거짓 중 하나라는 이가원리를 포기하는 것이며, 배중률을 포기하는 것은 아니다.)

이 오래된 수수께끼가 시사하는 바가 있다. 미래에 관한 진술과 시간에 따라 달라지는 진릿값을 다루려면, 문장 하나에 시간과 무관한 진릿값 하나를 붙이는 방식만으로는 부족하다는 것이다. 문제는 반드시 진릿값을 셋으로 늘려야 한다는 데 있는 것이 아니라, 참 또는 거짓이라는 진릿값이 시간에 영향을 받는다는 데에 있다. 아리스토텔레스에게는 이것을 담아낼 형식적 언어가 없었다. 인류가 그러한 언어를 얻기까지는 2300년을 더 기다려야 했다.

시제 연산자

시간과 진릿값의 관계를 다루는 언어를 만든 사람이 뉴질랜드의 논리학자 아서 프라이어(Arthur Prior)이다. 1950년대, 그는 시간과 운명과 신학을 둘러싼 오래된 질문들, 즉 아리스토텔레스의 해전, 신의 예지와 인간의 자유의지가 부딪히는 문제 같은 것들을 해결하기 위해 힘쓰고 있었다. 그러다 이 질문들을 제대로 다루려면 시제(tense)를 형식논리 안으로 들여와야 한다는 생각을 하게 된다. 그렇게 1957년 무렵 빚어낸 것이 시제논리(tense logic)이다. 오늘날 더 넓게는 시간논리(temporal logic)라고 부른다. 프라이어가 시제논리의 씨앗을 발표한 자리는 1957년 책 『Time and Modality』였다. 흥미롭게도 출발점은 순수논리가 아니라 신학과 형이상학이었다. 신의 예지가 인간의 자유와 어떻게 양립하는가 하는 질문이 그를 줄곧 끌고 갔다. 시간을 다루는 형식 언어 도구가 신학적 고민에서 자라났다는 점이 인상적이다.

프라이어의 발상은 산뜻하다. 일계논리처럼 시점을 양화 대상으로 끄집어내는 대신, 시제를 통째로 연산자로 만들어 버리는 것이다. 부정 \(\neg\)이 문장 앞에 붙어 새 문장을 만들듯, 시제 연산자도 문장 앞에 붙어 시간이 옮겨진 새 문장을 만든다. 프라이어는 기본 연산자 네 개를 고안하였다.

  • \(P\varphi\) : “과거에 \(\varphi\)였던 적이 있다.” (Past) 과거의 어느 시점에 \(\varphi\)가 참이었다.
  • \(F\varphi\) : “미래에 \(\varphi\)일 것이다.” (Future) 미래의 어느 시점에 \(\varphi\)가 참이 된다.
  • \(H\varphi\) : “과거에 늘 \(\varphi\)였다.” (Has always been) 과거의 모든 시점에 \(\varphi\)가 참이었다.
  • \(G\varphi\) : “앞으로 늘 \(\varphi\)일 것이다” (Going to be) 미래의 모든 시점에 \(\varphi\)가 참이다.

여기서 눈여겨볼 대응관계가 있다. \(P\)와 \(H\), 그리고 \(F\)와 \(G\)는 서로 양상의 짝(dual)을 이루며 대응된다. “과거의 어느 한 시점에 참”의 부정은 “과거의 모든 시점에 거짓”이니, 다음이 성립한다. \[ P\varphi \equiv \neg H\neg\varphi, \quad F\varphi \equiv \neg G\neg\varphi \] 양상논리를 공부했다면 이 꼴이 낯익을 것이다. 가능성 \(\Diamond\)와 필연성 \(\Box\)가 \(\Diamond\varphi \equiv \neg\Box\neg\varphi\)로 묶이는 바로 그 관계다. (여기서 \(\Diamond\)와 \(\Box\)는 글자가 깨진 것이 아니라, 양상논리에서 사용하는 기호이다.) 실제로 시제논리는 양상논리의 한 갈래로 볼 수 있다. \(F\)는 “접근 가능한 미래 시점 중 적어도 하나에서 참”인 가능성 연산자이고, \(G\)는 “접근 가능한 모든 미래 시점에서 참”인 필연성 연산자인 셈이다. 다만, 단일한 \(\Diamond ,\) \(\Box\)만 가진 기본 양상논리와 달리, 시제논리는 미래 방향과 과거 방향의 연산자를 한꺼번에 둔다. 과거를 보는 연산자와 미래를 보는 연산자가 따로 있는 것이다. 시간에는 방향이 있기 때문이다. \(P\)로 뒤를 돌아보는 일과 \(F\)로 앞을 내다보는 일은 같지 않다.

이 연산자들을 겹쳐 쓰면 보통의 양화로는 간단하게 표현하기 어려웠던 문장을 깔끔하게 표현할 수 있다. 몇 가지 예를 살펴보자.

  • \(FP\varphi\) : “미래의 어느 시점에 가서, 그 시점에서 과거를 돌아보면 \(\varphi\)였던 적이 있을 것이다.” 미래의 한 자리에서 다시 그 과거를 보는, 시점의 겹눈이다.
  • \(GF\varphi\) : “앞으로 어느 때가 되든, 그 뒤에 다시 \(\varphi\)가 참인 때가 온다.” 자연수 시간 위의 LTL에서는 이것을 “\(\varphi\)가 무한히 자주 일어난다”라고 읽을 수 있다.
  • \(\varphi \to GP\varphi\) : “지금 \(\varphi\)라면, 앞으로 늘 ‘\(\varphi\)였던 적이 있다’가 참이다.” 한번 일어난 일은 그 뒤로 영영 과거사로 남는다는, 시간의 한 방향성을 담은 문장이다.

마지막 문장은 특정한 시간 구조를 새로 가정한다기보다, \(P\)와 \(G\)가 같은 순서 \( < \)의 서로 반대 방향을 본다는 사실에서 나오는 기본 원리다. 정말로 시간의 모양에 따라 성립 여부가 갈리는 예는 다음 절의 \(FF\varphi \rightarrow F\varphi ,\) 그리고 \(F\varphi \rightarrow FF\varphi\) 같은 식에서 볼 수 있다.

시간에 의미를 입히다

지금까지는 연산자를 말로 풀어 읽기만 했다. “\(F\varphi\)는 미래의 어느 시점에 \(\varphi\)가 참”이라는 식으로 말이다. 그런데 ‘시점’이니 ‘미래’니 하는 말 자체가 모호할 수 있다. 시점이란 정확히 무엇이고, 한 시점이 다른 시점보다 미래라는 건 무슨 뜻인가? 시제논리에 단단한 바닥을 깔아 준 것이 크립키식 가능세계 의미론(Kripke semantics)이다. 양상논리에 쓰이던 그 틀이 시간 개념을 도입한 언어에서도 거의 그대로 들어맞는다.

기본 구조는 그리 복잡하지 않다. 시간을 한 쌍 \((T, <)\)으로 본다. 여기서 \(T\)는 시점들의 집합이고, \( < \)는 그 위의 이항관계로 ‘먼저’를 나타낸다. \(s < t\)는 시점 \(s\)가 시점 \(t\)보다 앞선다는 뜻이다. 양상논리에서 가능세계와 접근가능관계가 하던 역할을, 여기서는 시점과 시간순서가 맡는다. 다음으로, 각 시점마다 어떤 원자명제가 참인지 알려주는 진릿값 함수 \(V\)를 둔다. \(V(t)\)는 시점 \(t\)에서 참인 원자명제들의 모음이다. 이 셋을 묶은 \(\mathcal{M} = (T, <, V)\)가 하나의 모델이다.

이와 같은 모델이 바로 고전논리와 결정적으로 갈리는 대목이다. 진릿값이 모델 하나에 대해 정해지는 것이 아니라, 모델과 시점의 쌍에 대해 정해진다. 그래서 “\(\varphi\)가 참이다”가 아니라 “\(\varphi\)가 모델 \(\mathcal{M}\)의 시점 \(t\)에서 참이다”라고 말해야 하고, 이를 \(\mathcal{M}, t \models \varphi\)로 적는다. 우리가 글 첫머리에서 마주쳤던 그 성질, 즉 같은 문장이 때에 따라 참이 되기도 하고 거짓이 되기도 하는 성질이 의미론의 골격에 정식으로 들어앉은 것이다. 시점을 바꾸면 진릿값이 바뀐다.

이러한 구조를 바탕으로 진리 조건을 진술할 수 있다. 먼저 원자명제와 논리연결사는 고전논리 그대로다. 진릿값이 정해지는 시점만 \(t\)로 고정시켜 둔다. \[ \mathcal{M}, t \models p \;\iff\; p \in V(t) \] \[ \mathcal{M}, t \models \neg\varphi \;\iff\; \mathcal{M}, t \not\models \varphi \] \[ \mathcal{M}, t \models \varphi \wedge \psi \;\iff\; \mathcal{M}, t \models \varphi \;\text{그리고}\; \mathcal{M}, t \models \psi \] 시제논리의 맛은 시제 연산자에서 시작된다. 시제 연산자는 진릿값이 정해지는 시점을 \(t\)에서 다른 시점으로 옮긴다. \[ \mathcal{M}, t \models F\varphi \;\iff\; \text{어떤 } s > t \text{가 있어서}\; \mathcal{M}, s \models \varphi \] \[ \mathcal{M}, t \models G\varphi \;\iff\; t < s \text{인 모든 } s \text{에 대해}\; \mathcal{M}, s \models \varphi \] \[ \mathcal{M}, t \models P\varphi \;\iff\; \text{어떤 } s < t \text{가 있어서}\; \mathcal{M}, s \models \varphi \] \[ \mathcal{M}, t \models H\varphi \;\iff\; s < t \text{인 모든 } s \text{에 대해}\; \mathcal{M}, s \models \varphi \] 읽어 보면 시간에 대하여 우리가 가지고 있는 직관과 일치한다. \(F\varphi\)를 \(t\)에서 따지려면, \(t\)보다 뒤인 시점 \(s\) 가운데 \(\varphi\)가 참인 자리가 하나라도 있는지 보면 된다. \(G\varphi\)는 \(t\) 이후의 시점이 빠짐없이 \(\varphi\)를 만족해야 참이다. \(\exists\)와 \(\forall\)이 시간순서 \( < \)를 타고 미래 쪽으로 흐르는 것이다. \(P\)와 \(H\)는 똑같은 일을 하되 방향은 과거 쪽으로, 즉 \( < \)의 반대 방향으로 한다.

여기서 한 가지가 분명해진다. 시제논리의 연산자는 결국 시점에 대한 양화를 품고 있다. \(F\)와 \(P\) 안에는 \(\exists s\)가, \(G\)와 \(H\) 안에는 \(\forall s\)가 숨어 있다. 그러면 앞 절에서 본 일계논리 언어와 무엇이 다른가? 핵심은 양화의 위치이다. 일계논리에서는 양화사가 문장 표면에 드러나 우리가 손수 시점 변수를 다뤄야 했다. 시제논리에서는 양화가 연산자 안으로 숨고, 진릿값이 정해지는 시점 \(t\)는 의미론이 암묵적으로 떠받친다. 시점을 명시하지 않고도 시점에 대해 말하게 되는 셈이다. 우리가 시간을 겪는 방식, 즉 ‘지금’의 관점에서 앞뒤를 살피는 방식에 한결 가깝다.

시간의 모양

앞서 시제논리의 의미론을 다루며 관계 \( < \)에 아무 조건도 걸지 않았다. 그냥 이항관계라고만 했다. 그런데 시간을 떠올릴 때 우리는 은연중에 여러 성질을 가정한다. 시간은 한 방향으로 흐르고(\(s < t\)와 \(t < s\)가 같이 성립하진 않는다), \(a < b\)이고 \(b < c\)이면 \(a < c\)이며(추이성), 끊긴 곳 없이 빽빽하게 이어져 있고(조밀성), 과거와 미래 양쪽에 끝점이 없을 수도 있다. 이런 성질 하나하나를 \( < \)에 얹느냐 마느냐가 어떤 시제논리 문장을 참으로 만드느냐를 결정한다. 이와 관련된 성질 몇 가지를 살펴보자.

먼저 추이성(transitivity)이다. 모든 \(a,\, b,\, c\)에 대해 \(a < b\)이고 \(b < c\)이면 \(a < c\)라는 성질이다. 시간순서라면 응당 갖춰야 할 것 같은 이 성질에 다음 문장이 정확히 대응한다. \[ FF\varphi \to F\varphi \] “미래의 미래에 \(\varphi\)이면, 미래에 \(\varphi\)이다.” \( < \)가 추이적인 시간 위에서는 이 문장이 늘 참이고, 추이성이 깨진 시간 위에서는 거짓이 되는 모델을 만들 수 있다. 양상논리를 공부했다면 데자뷔를 느낄 것이다. 이것은 양상논리에서 추이성에 대응하던 공리 \[\Box\varphi \to \Box\Box\varphi\] 와 같은 골격이다.

다음으로 조밀성(density)을 살펴보자. 시제의 조밀성이란 임의의 두 시점 사이에 또 다른 시점이 늘 끼어 있다는 성질, 곧 \(s < t\)이면 \(s < u < t\)인 \(u\)가 있다는 것이다. 유리수 직선이나 실수 직선처럼 시간이 빽빽하게 이어진 그림이다. 이 성질에 대응하는 문장은 다음과 같다. \[ F\varphi \to FF\varphi \] 방금 본 추이성의 문장과 화살표 방향만 정확히 뒤집힌 꼴이라는 점이 눈에 띈다. 시간이 조밀하면 \(\varphi\)가 미래에 일어날 때 그 사이에 또 다른 미래 시점이 끼므로, “미래의 미래”로 한 번 더 밀어 넣을 수 있다. 만약 시간이 정수처럼 띄엄띄엄하다면 이 문장은 깨진다. 바로 다음 순간 \(\varphi\)가 일어나는데 그 ‘사이’에 낄 시점이 없는 경우가 생기기 때문이다.

여기서 한발 물러나 큰 그림을 보면, 시제논리에는 평행선 공준에서 보았던 것과 똑같은 상황이 있다. 기하학에서 평행선의 존재성과 관련된 공리를 어떻게 두는지에 따라 유클리드 기하학, 쌍곡기하학, 타원기하학이 구분된다. 시제논리에서는 시간순서 \( < \)에 어떤 성질을 부여하느냐에 따라 서로 다른 논리 체계가 구성된다. 시간을 조밀하게 보는 논리와 띄엄띄엄하게 보는 논리, 한 줄기로 흐른다고 보는 논리와 미래가 여러 갈래로 갈라진다고 보는 논리는 서로 다른 정리를 가진다. ‘단 하나의 옳은 시제논리’가 따로 있는 게 아니다. 시간을 어떻게 가정하느냐가 어떤 논리를 쓸지를 정한다. [특히 미래가 여러 갈래로 갈라진다고 보는 그림은 ‘Ockhamist 시간논리’나 분기시간논리(branching-time logic)로 이어지고, 이것은 다시 아리스토텔레스의 해전 문제와 곧장 맞닿는다. 미래가 가지를 친다면 “내일 해전이 일어날 것이다”의 진릿값은 어느 가지를 따라가느냐에 달리고, 미래가 아직 정해지지 않았다는 그림이 형식으로 살아난다. 뒤에서 만날 CTL은 이런 분기시간적 관점을 컴퓨터과학에서 다루는 대표적인 도구이다.]

선형시간논리

지금까지의 시제논리는 철학에서 태어났다. 그런데 1977년, 이 도구가 뜻밖의 곳에서 새 생명을 얻는다. 컴퓨터과학자 아미르 프누엘리(Amir Pnueli)가 프로그램의 동작을 따지는 데에 시간논리를 끌어들인 것이다. 발상의 씨앗은 간단하다. 돌아가고 있는 프로그램이란 결국 상태가 시간을 따라 줄줄이 바뀌어 가는 것이다. 그 ‘시간을 따라 바뀐다’라는 논리를 다루는 데 시간논리가 딱 맞춤이었던 것이다. (프누엘리는 이 공로로 1996년 튜링상을 받는다. 철학자들이 신학적 사변을 다루기 위해 만든 도구가, 수십 년 뒤 동시성 프로그램의 정확성을 증명하는 핵심 무기가 되었다. 순수한 사변을 통해 구성한 도구가 현실의 응용 문제를 해결하는데 사용되는 상황은 수학사에서 거듭 보는 장면이다.)

여기서 시간을 보는 관점이 살짝 달라진다. 컴퓨터과학에서 흔히 쓰는 시간의 모양은 선형시간(linear time)이다. 프로그램이 실행되는 단계를 떠올리면, 상태가 \(s_0,\) \(s_1,\) \(s_2,\) \(\dots\)로 수열처럼 흘러간다. 시간이 띄엄띄엄한 자연수처럼 놓이고, 각 순간에는 바로 다음 순간이 딱 하나 있다. 이렇게 시간을 한 줄로 보고 그 위에서 따지는 시간논리를 선형시간논리(Linear Temporal Logic), 줄여서 LTL이라 부른다.

주의할 점이 있다. 앞에서 프라이어식 시제논리를 설명할 때 \(F\)와 \(G\)는 현재를 제외한 엄격한 미래를 보았지만, LTL에서는 관례적으로 \(F\)와 \(G\)가 현재 상태를 포함한다. 즉 LTL의 \(F\varphi\)는 “지금 또는 나중에 \(\varphi\)”이고, \(G\varphi\)는 “지금부터 늘 \(\varphi\)”이다.

LTL은 프라이어의 시제 연산자를 컴퓨터과학에 맞게 손본다. 우선 보통은 미래만 본다. 프로그램의 앞날이 관심사이지 지나온 길은 대개 덜 중요하기 때문이다. 그리고 자연수처럼 띄엄띄엄한 시간을 다루기 위해 “바로 다음 순간”이라는 연산자를 새로 도입한다. 핵심 연산자는 다음과 같다.

  • \(X\varphi\) : “다음 순간(neXt)에 \(\varphi\)이다.” 바로 한 칸 뒤 상태에서 \(\varphi\)가 참이다.
  • \(F\varphi\) : “언젠가(Future)는 \(\varphi\)이다.” 지금이나 이후 어느 상태에서 \(\varphi\)가 참이 된다.
  • \(G\varphi\) : “늘(Globally) \(\varphi\)이다.” 지금부터 모든 상태에서 \(\varphi\)가 참이다.
  • \(\varphi\,U\,\psi\) : “\(\psi\)일 때까지(Until) \(\varphi\)이다.” 언젠가 \(\psi\)가 참이 되고, 그 전까지 줄곧 \(\varphi\)가 참이다.

여기서 \(U\)(until)가 LTL의 진짜 주인공이다. 프라이어의 네 연산자에는 없던 새 연산자이다. \(F\)와 \(G\)만으로는 잡아낼 수 없는 뉘앙스를 \(U\)가 잡아내기 때문이다. \(F\)는 “언젠가는 \(\psi\)”라고 말할 뿐, 그 언젠가에 이르기까지 무슨 일이 벌어지는지엔 입을 닫는다. \(U\)는 그 사이의 구간에 조건을 건다. \(\varphi\,U\,\psi\)는 두 가지를 한꺼번에 요구한다. \(\psi\)가 끝내 참이 될 것, 그리고 그 순간이 오기 전까지는 \(\varphi\)가 한 칸도 빠짐없이 버텨 줄 것. 사실 \(F\)는 \(U\)의 특수한 경우로 생각할 수 있다. “참인 무언가가 지속되다가 \(\psi\)에 이른다”는 \(\top\,U\,\psi\)가 곧 \(F\psi\)다. [그래서 LTL을 더 단순하게 정의하려면 \(X\)와 \(U\) 둘만 연산자로 두고 나머지를 정의로 끌어낸다. \(F\psi \equiv \top\,U\,\psi\)로 두고, \(G\varphi \equiv \neg F\neg\varphi\)로 둔다. “늘 \(\varphi\)”는 “\(\neg\varphi\)인 때가 결코 오지 않는다”와 같으니, 양상의 짝 관계가 여기서도 그대로 작동한다.]

이 연산자들이 진짜 힘을 쓰는 건 프로그램이 만족해야 할 성질을 표현할 때이다. 동시성 프로그램이나 시스템을 검증할 때 따지는 성질은 크게 두 갈래로 나뉘는데, LTL은 둘 다 깔끔하게 표현한다.

그 중 하나는 안전성(safety)이다. “나쁜 일은 결코 일어나지 않는다”와 같은 꼴의 성질이다. 이를테면 두 프로세스가 임계 구역(critical section)에 동시에 들어가는 일은 절대 없어야 한다. \(c_1\)과 \(c_2\)를 각각 두 프로세스가 임계 구역에 있다는 명제라 하면, 이 문장은 다음과 같이 표현된다. \[ G\,\neg(c_1 \wedge c_2) \] “모든 순간에, \(c_1\)과 \(c_2\)가 같이 참인 일은 없다.” \(G\)가 시간 전체에 걸쳐 금지 조항을 선언한다.

다른 하나는 생존성(liveness)이다. “좋은 일은 언젠가 일어난다”와 같은 꼴의 성질이다. 글 첫머리에서 명제논리로 옮기려다 실패한 그 문장, 즉 “요청이 들어오면 언젠가 응답이 온다”가 비로소 온전하게 표현된다. \[ G\,(\text{request} \to F\,\text{response}) \] 풀어 읽으면 이렇다. “모든 순간에 대해, 그 순간 요청이 들어오면, 그 순간이나 이후 어느 순간에 응답이 온다.” 바깥의 \(G\)가 ‘어느 순간에든’을 맡고, 안쪽의 \(F\)가 ‘언젠가’를 맡는다. 우리가 처음에 자연어로만 표현할 수 있었던 그 문장이, 두 시간 연산자를 겹쳐 한 줄로 또렷하게 표현된 것이다. 명제논리에 없던 것, 그리고 일계논리에서는 시점 양화로 무리하게 표현해야 했던 것이, 여기서는 연산자 두 개로 단정하게 표현된다.

조금 더 까다로운 성질도 표현할 수 있다. “요청이 무한히 자주 들어온다”라는 문장은 \(GF\,\text{request}\)로 표현할 수 있다. “어느 순간에 가도(\(G\)) 그 뒤에 또 요청이 온다(\(F\,\text{request}\))”라는 말이니, 요청이 영영 잦아들지 않는다는 뜻이다. 반대로 “언젠가부터는 줄곧 안정 상태다”는 \(FG\,\text{stable}\)로 적힌다. “어느 순간 이후로(\(F\)) 늘(\(G\)) 안정”이라는 구조를 가진 표현이다. \(GF\)와 \(FG\)는 연산자 두 개의 순서만 바뀌었는데 뜻이 사뭇 다르다. 시간 연산자는 이렇게 겹치는 순서가 곧 의미가 된다.

분기시간논리

LTL은 시간을 한 줄로 본다. 그런데 프로그램이 다음에 무엇을 할지가 여러 갈래로 갈리는 상황이라면 어떨까. 입력에 따라, 스케줄러의 변덕에 따라, 동시에 실행되는 프로세스들이 끼어드는 순서에 따라, 같은 상태에서 갈 수 있는 다음 상태가 여럿일 수 있다. 그러면 한 상태에서 뻗어 나가는 미래는 한 줄이 아니라 가지를 친 나무가 된다.

이처럼 갈라지는 미래를 다루는 것이 분기시간논리(branching-time logic)이다. 분기시간논리의 대표적인 예로 계산트리논리(CTL; Computation Tree Logic)를 들 수 있다. CTL은 ‘아리스토텔레스의 해전’에서 고려했던 논제와 같은 맥락을 공유한다. 즉 현 시점에서는 내일 해전이 일어나는 가지와 일어나지 않는 가지가 함께 뻗어 있고, 미래가 아직 한 줄로 정해지지 않았다.

가지가 갈리는 시간에서는 “미래에 \(\varphi\)이다”라는 말이 두 가지로 해석된다. 어느 한 갈래를 따라가면 \(\varphi\)에 이른다는 뜻일 수도 있고, 어느 갈래로 가든 \(\varphi\)에 이른다는 뜻일 수도 있다. 그래서 CTL에서는 갈래에 대한 양화사를 도입한다.

  • \(A\) : “모든 갈래에서(All paths)”를 나타내며, 지금 상태에서 뻗는 모든 미래의 길을 따라 진술의 상태가 된다는 뜻이다.
  • \(E\) : “어떤 갈래에서(Exists a path)”를 나타내며, 지금 상태에서 뻗는 미래의 길 가운데 진술의 상태가 되는 것이 적어도 하나 존재한다는 뜻이다.

이 갈래 양화사 \(A,\) \(E\)를 시간 연산자 \(X,\, F,\, G,\, U\) 앞에 붙여 문장을 구성한다. 이를테면 \(AG\varphi\)는 “모든 갈래의 모든 순간에 \(\varphi\)”로서, 닿을 수 있는 모든 상태에서 \(\varphi\)가 참이라는 강한 주장이다. \(EF\varphi\)는 “어떤 갈래의 어떤 순간에 \(\varphi\)”로서, \(\varphi\)인 상태에 닿는 길이 적어도 하나는 있다는 뜻이다.

  • \(AG\,\neg\text{error}\) : “어느 길로 가든, 어느 순간에도 오류 상태에 빠지지 않는다.” 시스템이 결코 고장 상태에 이르지 않음을 보증하는, 검증에서 가장 자주 쓰는 꼴이다.
  • \(AG\,EF\,\text{restart}\) : “닿을 수 있는 어느 상태에서든(\(AG\)), 거기서 다시 시작 상태로 돌아가는 길이 적어도 하나 있다(\(EF\)).” 어떤 상태에 도달하더라도, 그 곳에서 재시작 상태로 가는 경로가 하나 이상 존재한다.

여기서 LTL과 CTL의 차이가 도드라진다. LTL은 갈래 하나하나, 곧 실행 경로 하나하나를 놓고 “이 경로가 \(\varphi\)를 만족하는가”를 따진다. 시간이 한 줄이라는 전제 위에 서 있는 셈이다. CTL은 한 상태에서 뻗는 갈래 전체를 한눈에 놓고 “모든 갈래가 그런가, 아니면 그런 갈래가 있는가”를 따진다. (두 논리의 표현력은 어느 한쪽이 다른 쪽을 온전히 덮지 못한다. 예를 들어 LTL의 \(FG\varphi,\) 즉 “모든 실행에서 언젠가부터는 계속 \(\varphi\)”는 일반적으로 CTL로 표현되지 않는다. 반대로 CTL의 \(AG\,EF\,\varphi\)처럼 “도달 가능한 어느 상태에서든 \(\varphi\)에 이를 수 있는 어떤 갈래가 남아 있다”라는 성질은 LTL로 표현되지 않는다. 둘은 CTL∗ 안에 들어가는 서로 다른 문장이다.) 두 논리 중 어느 쪽이 맞느냐는 질문은 잘못된 질문이다. 시간을 한 줄로 보느냐 가지로 보느냐, 그 관점의 차이가 두 논리의 차이점이다. 즉 시간의 모양에 대한 가정에 따라 논리가 달라진다.

모델 검사

시간논리가 철학의 사변을 넘어 공학의 연장으로 자리 잡은 데에는 결정적 이유가 하나 있다. 시간논리가 단지 성질을 표현하는 데에 그치지 않고, 그 성질이 참인지를 기계가 자동으로 확인해 준다는 점이다. 이 기법을 모델 검사(model checking)라고 부른다.

밑그림은 이렇다. 검사하려는 시스템을 상태 집합 \(S,\) 전이관계 \(R,\) 라벨링 \(L\)로 이루어진 유한 Kripke 구조 \(K=(S,\,R,\,L)\)로 형식화한다. 이는 앞에서 본 시제논리 모델과 같은 계열의 의미론적 구조지만, 여기서 \(R\)은 보통 순서관계가 아니라 시스템의 가능한 한 단계 전이를 나타낸다. 모델 검사란 초기 상태 \(s_0\)에서 \(K, s_0 \models \varphi\)가 성립하는지를 자동으로 판정하는 절차다. LTL 명세는 보통 모든 실행 경로가 그 경로 공식을 만족하는지를 묻고, CTL 명세는 수식 안의 \(A,E\) 양화사에 따라 모든 경로 또는 어떤 경로를 따진다. 그렇게 따진 결과가 바라는 조건을 만족시키면 시스템은 그 성질에 관한 한 옳다. 그렇지 않으면, 검사기는 보통 \(\varphi\)를 깨뜨리는 실행 경로를 반례로 제시한다. CTL 명세의 모양에 따라서는 단일 경로가 아니라 작은 반례 구조나 증인 구조가 필요할 수도 있다. 어느 경우든 어디서 어떻게 어긋나는지를 보여주는 것이다.

이 성질이 모델 검사가 유용한 이유이다. 그냥 “틀렸다”가 아니라 “여기 이 순서로 일이 벌어지면 이렇게 잘못된다”를 짚어 주니, 설계의 빈틈을 곧장 메울 수 있다. 사람 손으로는 도무지 다 따라가 볼 수 없는, 수십억 갈래로 뻗는 동시성 시스템의 상태 공간을 기계가 빠짐없이 살피는 것이다. 1980년대에 에드먼드 클라크, 앨런 에머슨, 그리고 이들과는 독립적으로 연구하던 조지프 시파키스가 이 기법을 일궈냈고, 셋은 그 공로로 2007년 튜링상을 받는다. [모델 검사의 발목을 잡던 것은 줄곧 ‘상태 폭발(state explosion)’이었다. 변수와 프로세스가 몇 개만 늘어도 상태 수가 지수로 불어나 손쓸 수 없게 된다. 1990년 무렵 케네스 맥밀런 등이 상태 집합을 통째로 이진 결정 다이어그램(BDD)이라는 자료구조로 표현하는 기호적 모델 검사(symbolic model checking)를 내놓으면서, 다룰 수 있는 상태가 단숨에 천문학적 규모로 커졌다. 시간논리라는 언어가 있었기에 비로소 검사할 ‘대상’을 형식으로 표현할 수 있었고, 그 위에서 이런 알고리즘이 개발되었다.] 오늘날 CPU 제조사가 제품을 내보내기 전에 설계를 검증하고, 항공, 철도의 제어 시스템이 규격을 지키는지 확인하는 데 이 기법이 실제로 활용된다. 신학적 사변에서 자라난 언어가 사람의 목숨이 걸린 시스템의 무결성을 따지는 데에 사용되고 있는 것이다.

이야기를 마치며

지금까지 우리는 꽤 먼 길을 걸어왔다. 시제 연산자에서 시작하여 시간의 모양에 따라 논리가 달라질 수 있음을 확인하였고, 시간논리라는 도구가 프누엘리의 손에서 LTL로, 다시 분기시간을 품는 CTL로 자라나 끝내 프로그램을 검증하는 모델 검사로 발전하는 모습을 보았다.

이 여정에서 거듭 마주친 것이 있다. 당연하게 여기던 것을 다시 들여다봄으로써 크게 도약했다는 점이다. “진릿값은 시간과 무관하게 결정된다”라는 고전논리의 암묵적 전제를 의심하고, 진릿값이 시점에 따라 달라질 수 있는 가능성을 인정하는 순간, 닫혀 있던 문장의 세계가 열렸다. 평행선 공준 하나를 내려놓자 기하학이 여러 갈래로 갈라졌듯, 시간이 어떻게 생겼다는 가정 하나를 바꿀 때마다 새로운 논리가 모습을 드러냈다.

그리고 순수한 사변이 현실과 맞닿는 장면도 다시 보았다. 프라이어가 신의 예지와 자유의지를 논하기 위해 고안한 도구가, 반세기 뒤 동시성 프로그램의 정확성을 증명하는 언어가 되었다. 시간을 어떻게 다룰 것인가라는 질문은 논리학과 철학의 오랜 화두이면서, 동시에 오늘날 우리가 기대어 사는 시스템의 신뢰성을 떠받치는 살아 있는 주제이다. 우리가 겪는 시간이 정말 한 줄로 흐르는지, 아니면 매 순간 갈라지는지, 끊긴 데 없이 이어지는지 아니면 띄엄띄엄한지, 이 오래된 물음에 마음이 끌린다면, 시간논리의 세계로 한 발 더 들어가 보기 바란다.

참고문헌

더 깊이 들어가 보고 싶은 독자에게 권할 만한 문헌을 모았다. 시제논리는 철학과 논리학에서 출발해 컴퓨터과학으로 흘러간 분야라, 읽을거리도 자연스럽게 그 두 갈래로 나뉜다. 본문에서 맛만 본 개념을 제대로 펼쳐 보고 싶다면 아래 문헌들이 도움이 될 것이다.

먼저 시제논리의 뿌리에 해당하는 철학, 논리학 문헌이다.

  • Prior, A. N. (1957). 『Time and Modality』. Oxford: Clarendon Press. — 프라이어가 1956년 옥스퍼드 존 로크 강연을 바탕으로 펴낸 책으로, 프라이어의 시제논리를 책 형태로 널리 알린 초기 핵심 저작이다. 본문에서 본 네 연산자 \(P,\) \(F,\) \(H,\) \(G\)를 소개한 책이다.
  • Prior, A. N. (1967). 『Past, Present and Future』. Oxford: Clarendon Press. — 프라이어의 대표작이자 『Time and Modality』의 후속편. 분기시간을 비롯해 본문에서 다룬 거의 모든 주제를 체계적으로 전개한다.
  • Kripke, S. A. (1963). “Semantical Considerations on Modal Logic.” Acta Philosophica Fennica, 16, 83–94. — 양상논리의 가능세계 의미론을 제시한 논문이다. 본문의 시점 상대적 의미론은 Kripke식 관계 의미론을 시간 구조에 적용한 것이다.

다음은 이 도구가 컴퓨터과학으로 건너오면서 나온 논문들이다.

  • Pnueli, A. (1977). “The Temporal Logic of Programs.” Proceedings of the 18th Annual Symposium on Foundations of Computer Science (FOCS), 46–57. — 시간논리를 프로그램 검증에 처음 끌어들인 논문. 본문에서 ‘뜻밖의 곳에서 새 생명을 얻는다’라고 한 바로 그 전환점이다. 프누엘리는 이 공로로 1996년 튜링상을 받았다.
  • Clarke, E. M., & Emerson, E. A. (1981). “Design and Synthesis of Synchronization Skeletons Using Branching-Time Temporal Logic.” In 『Logics of Programs』 (Lecture Notes in Computer Science, vol. 131, pp. 52–71). Springer. — CTL과 모델 검사라는 발상이 함께 등장한 논문이다. 분기시간 위에서 동시성 프로그램을 자동으로 검증하는 길을 열었다.
  • Queille, J.-P., & Sifakis, J. (1982). “Specification and Verification of Concurrent Systems in CESAR.” In 『Proceedings of the 5th International Symposium on Programming』 (Lecture Notes in Computer Science, vol. 137, pp. 337–351). Springer. — 클라크, 에머슨과는 독립적으로, 거의 같은 시기에 모델 검사 기법(CESAR 시스템)을 고안한 논문. 세 사람이 2007년 튜링상을 공동 수상한 배경이다.
  • Emerson, E. A., & Halpern, J. Y. (1986). “‘Sometimes’ and ‘Not Never’ Revisited: On Branching versus Linear Time Temporal Logic.” Journal of the ACM, 33(1), 151–178. — LTL과 CTL의 표현력이 서로를 대체하지 못한다는 사실을 정리하고, 둘을 아우르는 CTL∗를 제시한 고전. 본문에서 두 논리를 비교한 대목의 근거가 되는 논문이다.

마지막으로 더 깊이 공부하고 싶은 독자를 위한 교재와 개괄서다. 위 논문을 읽기 전에 먼저 보면 한결 수월하다.

  • Blackburn, P., de Rijke, M., & Venema, Y. (2001). 『Modal Logic』. Cambridge: Cambridge University Press. — 현대 양상논리의 표준 교재. 본문에서 슬쩍 언급한 대응 이론을 다룬다. 시제논리를 양상논리의 한 갈래로 보는 관점을 다지기에 좋다.
  • Goldblatt, R. (1992). 『Logics of Time and Computation』 (2nd ed.). Stanford: CSLI Publications. — 시제논리에서 계산 이론으로 건너가는 과정을 간결하게 설명한 책. 분량이 얇아 학부생도 부담 없이 읽을 만하다.
  • Clarke, E. M., Grumberg, O., & Peled, D. A. (1999). 『Model Checking』. Cambridge, MA: MIT Press. — 모델 검사 분야를 처음으로 한 권에 정리한 표준 교재다. LTL, CTL, 그리고 검사 알고리즘과 상태 폭발 문제까지 다룬다.
  • Baier, C., & Katoen, J.-P. (2008). 『Principles of Model Checking』. Cambridge, MA: MIT Press. — 더 현대적이고 친절한 모델 검사 교재. LTL, CTL의 의미론과 알고리즘을 차근차근 설명하므로, 본문을 읽고 제대로 공부를 시작하려는 독자에게 특히 권할 만하다.
  • McMillan, K. L. (1993). 『Symbolic Model Checking』. Kluwer Academic Publishers. — 기호적 모델 검사를 설명한 책. 상태 집합과 전이관계를 BDD로 상징적으로 표현하여 상태 폭발 문제를 크게 완화하는 기호적 모델 검사를 소개한다.
  • Øhrstrøm, P., & Hasle, P. F. V. (1995). 『Temporal Logic: From Ancient Ideas to Artificial Intelligence』 (Studies in Linguistics and Philosophy, vol. 57). Dordrecht: Kluwer Academic Publishers. — 이 글이 소개하는 내용을 통째로 담은 역사서이다. 아리스토텔레스의 해전과 중세 논리학에서 출발해, 프라이어를 지나 컴퓨터과학과 자연어 처리에서의 쓰임까지 이어진다. 이 글의 흐름을 더 자세히 보고 싶다면 가장 먼저 권하고 싶은 책이다.

온라인에서 무료로 볼 수 있는 자료로는 스탠퍼드 철학 백과사전(Stanford Encyclopedia of Philosophy)의 ‘Temporal Logic’ 항목(Goranko & Rumberg)을 권한다. 아리스토텔레스의 미래 우연 명제부터 현대 시간논리까지 최신 흐름을 균형 있게 짚어 주어, 어디서부터 시작할지 막막한 독자에게 좋은 길잡이가 된다.

🍭

Focus Mode