---
id: MATH-RES-2026-05-001
title: Temporal Logic (시간 논리)
category: "10_Wiki/Topics/Mathematics & Logic"
status: verified
confidence_score: 0.99
tags: [logic, math, formal-verification, concurrency, computer-science]
created_at: 2026-05-08
updated_at: 2026-05-08
---

# Temporal Logic (시간 논리)

## 📌 한 줄 통찰 (The Karpathy Summary)
> "시간의 흐름을 기술하는 수학적 언어: 정적인 참/거짓을 넘어, '결국 ~가 될 것이다(Eventually)', '항상 ~이다(Always)', '~할 때까지(Until)'와 같은 시점의 개념을 논리식에 도입하여 동적 시스템의 명세를 정의하는 틀."

## 📖 구조화된 지식 (Synthesized Content)
*   **선형 시간 논리 (LTL, Linear Temporal Logic)**: 시간을 하나의 경로(Path)로 간주한다. 미래의 특정 시점이나 범위에 대한 조건을 정의하는 데 유용하며, 프로그램의 실행 흐름을 검증할 때 주로 사용된다.
*   **계층 시간 논리 (CTL, Computation Tree Logic)**: 시간을 여러 갈래로 뻗어나가는 트리(Tree) 구조로 간주한다. "모든 경로에서 ~가 발생한다" 또는 "어떤 경로에서는 ~가 가능하다"와 같은 분기적(Branching) 특성을 기술할 수 있다.
*   **주요 연산자**:
    *   **G (Global)**: 항상 만족함.
    *   **F (Future)**: 언젠가 한 번은 만족함.
    *   **X (Next)**: 바로 다음 시점에 만족함.
    *   **U (Until)**: 특정 조건이 충족될 때까지 지속됨.

## ⚖️ 트레이드오프 및 고려사항
*   **표현력 vs 결정 가능성**: 논리가 복잡해질수록(예: 고차 논리 결합) 표현력은 좋아지지만, 해당 논리식이 참인지 거짓인지 판별하는 알고리즘의 복잡도가 기하급수적으로 증가하거나 판별 불가능해질 수 있다.
*   **형식 검증 (Formal Verification)**: 시스템의 안전성(Safety)과 활성(Liveness)을 증명하는 데 강력하지만, 실제 대규모 소프트웨어에 적용하기에는 명세 작성 비용이 매우 높다.
*   **실무적 적용**: 주로 하드웨어 설계 검증, 분산 알고리즘의 무한 루프 방지, 자율 주행 에이전트의 제약 조건 설정 등에 부분적으로 활용된다.

## 🔗 지식 연결 (Graph)
- **상위 개념**: [[Mathematical Logic]], [[Formal Methods]]
- **유사 개념**: [[Modal Logic]], [[Model Checking]], [[State Transition Systems]]
- **관련 기술**: [[TLA+ (Temporal Logic of Actions)]], [[Spin (Model Checker)]], [[NuSMV]]

---
*Last updated: 2026-05-08*

