경로 지도를 통한 오토마타 이론 이해

Source: Dev.to

형식 검증 및 자동자 이론

형식 검증은 소프트웨어가 올바르게 동작함을 보장하기 위해 사용되는 기법입니다. 형식 검증에서는 시스템의 동작을 수학적으로 모델링하고, 만족해야 할 사양을 논리식으로 표현합니다.

단순히 상태를 나열하는 것이 아니라, 목표는 다음과 같습니다:

• 사양을 수학적 모델로 표현하기
• 이러한 사양이 항상 만족되는지 혹은 위배되는지를 기계적으로 판단하기
• 테스트로 놓치기 쉬운 경우를 포함하여 안전성을 보장하기

자동자 이론은 이러한 목표를 달성하기 위한 도구로 사용됩니다.

자동자가 압도적으로 느껴질 수 있는 이유

이 분야에서는 DFA, NFA, NBA, LTL와 같은 기술 용어가 연속해서 등장하여 혼란스러울 수 있습니다. “상태 전이”, “비결정성”, “무한 실행”과 같은 추상적인 개념은 처음에는 크게 이해되지 않을 수 있습니다.

이러한 아이디어를 열차 노선도 비유로 시각화하면 형식 검증이 어떻게 작동하는지 직관적으로 이해하는 데 도움이 될 수 있습니다.

대상 독자

• 대학에서 자동자 이론이나 형식 검증을 막 시작한 학생
• 모델 검증이나 LTL 수업에서 “대충 이해는 하는데 아직 감이 안 잡힌다”는 느낌을 받는 학습자
• 시스템 검증에 관심이 있는 엔지니어

두 가지 기본 관점

오토마타를 이해하려 할 때, 실제로 기억해야 할 두 축만 존재합니다:

이 축들을 조합하면 오토마타는 이론적으로 네 종류로 분류될 수 있습니다:

결정성, 비결정성, 그리고 무한 실행이 무엇인지에 대해서는 구체적인 예시와 함께 나중에 설명합니다.

Note: DBA (deterministic Büchi automata) – 결정적 무한 실행을 다루는 경우 – 는 여기서 생략합니다. 표현력과 실용성 측면에서 거의 필요하지 않기 때문입니다.

가장 간단한 경우: DFA (Deterministic Finite Automaton)

DFA는 가장 직관적인 자동자입니다. 경로‑지도 비유에서는 단일 라인 경로에 해당합니다.

예시 경로

Start ──Green Line──► G0 ──Green Line──► Goal

특징

• 역(상태): Start, G0, Goal
• 선로(전이): 각 역에서 다음 역으로 연결되는 경로
• 티켓(입력): “Green Line을 타는” 행동

핵심 포인트: 현재 역에 있을 때 정확히 하나의 다음 역만으로 이동할 수 있다는 점입니다. Start에서 Green Line을 타면 언제나 G0에 도착합니다. 다른 선택지는 존재하지 않습니다.

형식적 정의

DFA는 5‑튜플

[ A = (Q,; q_0,; \Sigma,; \delta,; F) ]

이 정의는 상태‑전이 다이어그램으로 시각화할 수 있습니다. 교과서에서는 다이어그램 자체를 종종 “자동자”라고 부릅니다. 엄밀히 말하면 자동자는 전체 튜플을 의미하며, 이러한 튜플이 여러 개 모인 것을 *자동자들(automata)*이라고 합니다.

NFA (비결정적 유한 자동자) 로 확장

“DFA”의 D는 Deterministic(결정적)을 의미합니다; 이를 Nondeterministic(비결정적)으로 바꾸면 NFA가 됩니다. 이제 여러 가능한 다음 상태가 존재할 수 있습니다.

경로‑지도 비유

Start ──Green Line──► G1 ──Green Line──► Goal
          │
          └─Blue Line──► B1 ──(Green/Blue)──► Goal

• Start에서 G1(Green) 또는 B1(Blue)으로 갈 수 있습니다.
• G1에서 직접 Goal(Green) 또는 B1(Blue)으로 갈 수 있습니다.
• B1에서 다시 G1과 Goal 사이를 선택할 수 있습니다.

비결정성은 정확히 어떤 경로가 선택될지는 그 순간에 결정되지 않음을 의미합니다. NFA는 가능한 경로 중 최소 하나가 수용 상태에 도달하면 입력을 수용합니다.

Source: …

NBA (Nondeterministic Büchi Automaton) – 무한 실행 처리

NBA는 무한 행동을 다루기 위해 NFA를 확장한 것입니다. 경로 지도 비유에서는 이것이 영원히 순환할 수 있는 원형 노선에 해당합니다.

예시: 원형 라인

S0 ──► S1 ──► S2 ──► … ──► S7 ──► S0 (repeat)

• 이 라인에는 8개의 역(유한)만 존재하지만 무한히(무한 시간) 순환할 수 있습니다.

NBA는 바로 이러한 무한 실행을 정확히 포착합니다. 많은 프로그램과 시스템은 “시작되면 영원히 실행”되기 때문에, 이를 분석하려면 NBA가 필요합니다.

중요: 무한성은 상태의 개수가 아니라 실행 시간에 있습니다. NBA는 무한 시간 행동을 나타내기 위해 유한한 상태 집합을 사용합니다.

Source: …

핵심 관점 요약

1. Deterministic vs. Nondeterministic
2. Finite vs. Infinite execution

자동이론을 처음 배울 때 나는 1번과 2번을 혼동해서, 무한 실행이면 반드시 무한히 많은 서로 다른 결과가 나올 것이라고 잘못 생각했다. 실제로는 가능한 전이가 많이 있더라도, 전이를 적절히 그룹화하면 상태의 수는 유한하게 유지된다.

우리는 “무한을 유한으로 바꾸는” 것이 아니다.
우리는 유한한 상태 수를 가진 자동자를 사용해 무한 시간 행동을 결정 가능하게 만들고 있는 것이다.

트래픽 라이트 예시

신호등은 세 가지 상태를 가집니다

상태 전이는 다음과 같습니다:

[Green]  --time passes-->  [Yellow]  --time passes-->  [Red]  --time passes-->  [Green]  --> …

이는 무한히 반복되는 사이클을 형성합니다.

신호등을 결정적 유한 자동장치 (DFA) 로 표현하면, 각 순간의 상태가 결정적으로 정의됩니다. 예를 들어 현재 상태가 Green이면 다음 상태는 항상 Yellow가 됩니다.

신호등이 영원히 작동하므로 이를 비결정적 부히 자동장치 (NBA) 로 모델링하는 것이 자연스럽습니다. 무한 루프 Green → Yellow → Red → Green → … 은 단 세 개의 상태만으로 표현할 수 있습니다.

시스템 동작에서 명세로

지금까지 우리는 시스템이 어떻게 동작하는지를 설명했습니다.
다음 단계는 시스템이 올바르게 동작하는지 여부를 확인하는 것입니다. 이를 위해 선형 시계 논리 (LTL) 를 사용합니다.

LTL은 시간에 관한 명세를 작성하기 위한 논리입니다. 경로 지도 비유를 사용하면, 이는 “운용 규칙”을 설명합니다; 교통 신호등의 경우, 색상이 어떻게 변하는지에 대한 “규칙”을 기호 연산자를 사용해 기술합니다.

LTL 연산자

Note: Globally와 Finally는 기본 연산자가 아니며, U와 부정(¬)으로부터 파생됩니다.

G p ≡ ¬F ¬p
F p ≡ true U p

이 연산자들을 결합함으로써 복잡한 시계적 속성을 표현할 수 있습니다.

교통 신호등에 대한 LTL 명세 예시

1. “빨간불이 켜지면, 그 뒤에 초록불이 켜져야 한다.”

   G (Red → X Green)

2. “빨간불과 초록불이 동시에 켜지는 상태가 없어야 한다.”

   G ¬ (Green ∧ Red)

3. “시간이 얼마나 지나든, 초록불은 반복해서 나타나야 한다.”

   GF Green          // always eventually green

LTL은 사람이 쓰기에는 쉽지만, 컴퓨터는 더 기계적으로 다루기 쉬운 형태가 필요합니다: NBA.

LTL을 NBA로 변환

수학적으로 모든 LTL 명세는 동등한 NBA로 변환될 수 있음이 증명되었습니다 (LTL이 ω‑regular languages 클래스에 속하기 때문입니다).

예시: 명세 “green appears infinitely often” (GF Green)를 다음과 같은 NBA로 변환할 수 있습니다:

S1 (start) ──[¬Green]──► S1
   │
   └─[Green]──► S2 ──► S1

• S1에서 자동자는 현재 심볼이 Green인지 not Green인지 확인합니다.
• Green을 보면 S2로 이동하여 해당 발생을 받아들이고, 다음 단계에서 다시 S1으로 돌아갑니다.
• not Green을 보면 S1에 머무릅니다.

이 NBA는 Green을 무한히 통과하는 실행만을 정확히 받아들입니다.

Source: …

모델 검증 절차

1. 실제 시스템을 상태 전이 다이어그램(또는 NBA)으로 표현한다.
2. 명세를 LTL로 작성한다.
3. LTL 공식을 NBA로 변환한다.
4. 시스템 NBA와 명세 NBA의 **곱(product)**을 만든다.
5. 곱 자동화에서 수용 가능한 무한 경로가 있는지 탐색한다.

그러한 경로가 존재하면 반례(버그)이며,
수용 가능한 경로가 없으면 시스템이 명세를 만족한다.

교통신호등 예시

형식 검증이 중요한 이유

• 버그 탐지: 전통적인 테스트로는 찾기 어려운 타이밍‑의존적이고 드문 경우의 버그를 전면적으로 탐색합니다.
• 안전 보장: 안전‑중요 분야(예: 항공, 의료 기기)에서는 버그가 없다는 수학적 증명이 필요합니다.
• 명세 명확화: 요구사항을 LTL로 작성하면 시스템이 보장해야 할 내용이 정확하고 모호함 없이 정의됩니다.

경로‑지도 비유를 사용하면 자동자 이론의 전문 용어가 더 직관적으로 다가옵니다. 형식 검증은 처음에 다소 벅차 보일 수 있지만, 그 핵심은 단순합니다:

1. 시스템이 어떻게 동작하는지 기술 (자동자).
2. 시스템이 만족해야 할 규칙을 기술 (LTL → NBA).
3. 기계적으로 검증 (곱 자동자 + 공집합 테스트).

자동자가 이 목적을 위한 도구라는 점을 이해하면 주제가 훨씬 접근하기 쉬워집니다.

더미를 위한 자동자 이론 기초

선형 시간 속성 및 선형 시계 논리 (LTL)의 자동자 기반 표현