Towards the Usage of Window Counting Constraints in the Synthesis of Reactive Systems to Reduce State Space Explosion

1. 문제 정의 (Problem)

반응형 시스템 (Reactive Systems) 의 합성 (Synthesis) 은 환경과 상호작용하는 시스템에 대한 자동화된 전략을 생성하는 것을 목표로 합니다. 그러나 이 과정은 상태 공간 폭발 (State Space Explosion) 문제로 인해 많은 응용 분야에서 비효율적입니다.

• 기존 한계: 시스템 명세 (LTL 등) 를 결정적 오토마타로 변환하는 과정은 명세 길이에 대해 이중 지수적 (doubly exponential) 인 복잡도를 가집니다. 이로 인해 전략 합성이 많은 실제 응용 사례에서 불가능해집니다.
• 특수한 제약의 부재: 기존의 효율적인 합성 알고리즘 (예: GR(1) 클래스) 은 특정 명세 패턴에 국한되어 있으며, 시스템 행동의 빈도나 반복성을 나타내는 카운팅 패턴 (Counting Patterns) 을 포함한 명세에 대한 효율적인 합성 방법은 아직 충분히 연구되지 않았습니다.
• 목표: 카운팅 제약 (Counting Constraints) 을 가진 명세에 대해 상태 공간 폭발을 줄이고 합성 효율성을 높이는 새로운 접근법 개발.

2. 방법론 (Methodology)

저자들은 윈도우 카운팅 제약 (Window Counting Constraints) 을 도입하고, 이를 활용한 점진적 합성 (Incremental Synthesis) 알고리즘을 제안합니다.

2.1. 윈도우 카운팅 제약 (Window Counting Constraints)

시스템이 특정 행동 (action) 을 일정 기간 (윈도우) 내에 얼마나 자주 수행해야 하는지 (또는 수행하지 않아야 하는지) 를 정의합니다.

• 형식: "시스템이 자신의 $l$ 번의 행동 중 $k$ 번 이상 (또는 이하) 행동 $act$ 를 수행한다."
  • 예: $CC_{min}(p, a, k, l)$: 플레이어 $p$ 가 $l$ 번 중 $k$ 번 이상 행동 $a$ 를 수행.
  • 예: $CC_{max}(p, a, k, l)$: 플레이어 $p$ 가 $l$ 번 중 $k$ 번 이하로 행동 $a$ 를 수행.
• 합리적 환경 가정: 환경 (ALTER) 도 자신의 카운팅 제약을 준수한다는 가정 하에 합성을 수행합니다. 이는 시스템이 환경을 제재하여 이기는 것이 아니라, 환경의 합리적 행동을 전제로 전략을 수립함을 의미합니다.

2.2. 점진적 합성 알고리즘 (Incremental Synthesis)

전체 명세를 한 번에 변환하여 오토마타를 만드는 대신, 제약의 파라미터 (특히 윈도우 길이 $l$) 를 점진적으로 늘려가며 합성을 수행합니다.

1. 단순화된 제약으로 시작: 카운팅 제약의 윈도우 길이 ($l$) 를 최소값으로 설정하여 작은 상태 공간의 게임 그래프를 생성합니다.
2. 승리 영역 (Winning Region) 분석: 현재 제약 하에서 시스템 (EGO) 이 승리할 수 있는 상태 영역을 계산합니다.
3. 점진적 확장 (Increment): 제약의 윈도우 길이를 늘립니다.
   • 단조성 (Monotonicity) 활용:
     • $CC_{min}$ (최소 횟수): 더 짧은 윈도우에서 승리하는 전략은 더 긴 윈도우에서도 유효합니다.
     • $CC_{max}$ (최대 횟수): 더 긴 윈도우에서 승리하는 전략은 더 짧은 윈도우에서도 유효합니다 (또는 논리적 변환을 통해 $CC_{min}$ 으로 변환).
   • 상태 공간 축소: 이전 단계에서 계산된 승리 영역을 기반으로, 다음 단계의 상황 그래프 (Situation Graph) 를 구성할 때 불필요한 부분 (이미 승리/패배가 확정된 상태의 확장) 을 제거하거나 생략합니다.
4. 수렴: 제약이 원래 명세와 일치할 때까지 이 과정을 반복하거나, 중간 단계에서 승리 전략이 발견되면 종료합니다.

2.3. 상황 그래프 (Situation Graph)

기존의 게임 그래프에 카운팅 제약을 만족시키기 위한 '기억 (History)' 정보를 인코딩한 확장된 그래프입니다. 점진적 합성에서는 이 그래프를 처음부터 완전히 구축하지 않고, 이전 단계의 정보를 활용하여 필요한 부분만 동적으로 구축합니다.

3. 주요 기여 (Key Contributions)

1. 윈도우 카운팅 제약의 도입: 반응형 시스템 합성에서 시스템 행동의 빈도/횟수를 제어하는 새로운 제약 유형을 정의하고 이를 게임 이론적 프레임워크에 통합했습니다.
2. 점진적 합성 프레임워크 제안: 카운팅 제약의 단조성 (Monotonicity) 을 이용하여, 작은 제약에서 시작해 점진적으로 확장하는 알고리즘을 제시했습니다. 이는 전체 상태 공간을 한 번에 구축하는 전통적인 방식 대비 메모리 및 계산 시간을 크게 절감합니다.
3. 다양한 승리 조건 지원: 기존 연구 (안전 게임) 를 넘어 도달 가능성 (Reachability), Büchi, co-Büchi, Parity 게임 등 다양한 승리 조건을 지원하는 확장된 알고리즘을 제시했습니다.
4. 이론적 기반 및 변환: $CC_{max}$ (최대 횟수) 제약을 $CC_{min}$ (최소 횟수) 제약으로 변환하는 논리를 통해, 모든 제약을 동일한 점진적 증가 로직으로 처리할 수 있도록 했습니다.

4. 실험 결과 (Results)

저자들은 Python 으로 구현된 알고리즘을 다양한 테스트 케이스 (그리드 기반 로봇 이동 시나리오 등) 에 적용하여 성능을 평가했습니다.

• 비교 대상: 점진적 합성 (Sequential 및 Round-robin 모드) vs. 전체 제약 길이로 직접 합성 (비점진적).
• 성능 향상: 대부분의 실험에서 점진적 합성이 계산 시간과 메모리 사용량 측면에서 비점진적 방식보다 월등히 우수했습니다.
  • 예: 실험 2 의 경우, 비점진적 방식은 약 6,000 초 (6,097,599 상태) 가 소요된 반면, 점진적 방식 (Round-robin) 은 3 초 (9,742 상태) 만에 해결했습니다.
  • 실험 4 와 5 의 경우, 비점진적 방식은 메모리 한계 (Thrashing) 로 인해 실행이 중단되었으나, 점진적 방식은 성공적으로 전략을 생성했습니다.
• 예외 사항: 일부 게임 (예: 실험 7) 의 경우, 초기 단계에서 승리 영역이 비어 있어 점진적 방식의 오버헤드가 발생하여 전통적인 방식보다 느리기도 했습니다. 이는 전체 제약 길이가 필수적인 경우 발생할 수 있는 한계입니다.

5. 의의 및 향후 과제 (Significance & Future Work)

• 의의:

  • 반응형 시스템 합성의 핵심 병목 현상인 상태 공간 폭발을 해결하기 위한 실용적인 휴리스틱을 제공합니다.
  • 로봇 공학, 자동화 시스템 등에서 빈번하게 발생하는 "주기적 행동"이나 "빈도 제한" 명세를 효율적으로 처리할 수 있는 길을 열었습니다.
  • 명세 변환의 복잡성을 줄이지는 않지만 (복잡도 클래스는 동일), 실제 실행 가능한 크기의 문제를 해결할 수 있게 합니다.

• 향후 과제:

  1. 협력적 게임 (Cooperative Games) 으로 확장: 현재는 제로섬 (Zero-sum) 게임에 국한되어 있으며, 환경의 제약을 위반하지 않고 상호 협력하는 시나리오로 확장 계획.
  2. 새로운 명세 패턴 발견: 카운팅 제약과 유사한 단조성 (Monotonicity) 을 가진 다른 명세 패턴 (예: "x 가 발생하면 k 번 이내에 y 발생") 을 찾아 알고리즘에 적용.
  3. 심볼릭 합성 (Symbolic Synthesis): 명시적 상태 표현 대신 BDD 나 Antichain 등을 활용한 심볼릭 방식으로 변환하여 대규모 시스템 적용성 확보.
  4. 온더플라이 (On-the-fly) 합성과의 결합: 상태 공간을 동적으로 탐색하는 기존 알고리즘과 본 점진적 접근법을 결합.
  5. 대칭적 합성 (Symmetric Synthesis): 동일한 하드웨어/소프트웨어를 가진 다수의 시스템 (예: 로봇 군집) 에 동일한 전략을 적용하는 문제 해결.

이 논문은 복잡한 명세를 가진 반응형 시스템의 합성 문제를 해결하기 위해, 명세의 구조적 특성을 활용하여 점진적으로 문제를 단순화하고 해결하는 혁신적인 접근법을 제시했다는 점에서 의의가 큽니다.