2025-11-23T10:46:16.032830

Strategy Templates for Almost-Sure and Positive Winning of Stochastic Parity Games towards Permissive and Resilient Control

Phalakarn, Pruekprasert, Hasuo
Stochastic games are fundamental in various applications, including the control of cyber-physical systems (CPS), where both controller and environment are modeled as players. Traditional algorithms typically aim to determine a single winning strategy to develop a controller. However, in CPS control and other domains, permissive controllers are essential, as they enable the system to adapt when additional constraints arise and remain resilient to runtime changes. This work generalizes the concept of (permissive winning) strategy templates, originally introduced by Anand et al. at TACAS and CAV 2023 for deterministic games, to incorporate stochastic games. These templates capture an infinite number of winning strategies, allowing for efficient strategy adaptation to system changes. We focus on two winning criteria (almost-sure and positive winning) and five winning objectives (safety, reachability, Büchi, co-Büchi, and parity). Our contributions include algorithms for constructing templates for each winning criterion and objective and a novel approach for extracting a winning strategy from a given template. Discussions on comparisons between templates and between strategy extraction methods are provided.
academic

확률적 패리티 게임의 거의 확실한 승리 및 양의 확률 승리를 위한 전략 템플릿: 허용적이고 탄력적인 제어를 향하여

기본 정보

  • 논문 ID: 2409.08607
  • 제목: Strategy Templates for Almost-Sure and Positive Winning of Stochastic Parity Games towards Permissive and Resilient Control
  • 저자: Kittiphon Phalakarn, Sasinee Pruekprasert, Ichiro Hasuo
  • 분류: eess.SY cs.LO cs.SY
  • 발표 시간: 2024년 9월 (arXiv v2: 2025년 10월 16일)
  • 논문 링크: https://arxiv.org/abs/2409.08607

초록

확률적 게임은 다양한 응용 분야에서 기초적인 역할을 하며, 특히 사이버-물리 시스템(CPS) 제어에서 제어기와 환경이 게임 참여자로 모델링된다. 전통적인 알고리즘은 일반적으로 제어기를 개발하기 위한 단일 승리 전략을 결정하는 것을 목표로 한다. 그러나 CPS 제어 및 기타 분야에서는 추가 제약 조건이 발생할 때 시스템이 적응하고 런타임 변화에 대해 탄력성을 유지할 수 있도록 하는 허용적 제어기가 중요하다. 본 연구는 전략 템플릿 개념을 확정적 게임에서 확률적 게임으로 일반화하며, 이러한 템플릿은 무한한 수의 승리 전략을 포착하여 시스템 변화에 대한 효율적인 전략 적응을 가능하게 한다. 우리는 두 가지 승리 기준(거의 확실한 승리 및 양의 확률 승리)과 다섯 가지 승리 목표(안전성, 도달성, Büchi, co-Büchi 및 패리티)에 중점을 둔다.

연구 배경 및 동기

문제 배경

  1. 전통적 방법의 한계: 전통적인 게임 해결 알고리즘은 일반적으로 단일 승리 전략만 찾으며 전략의 허용성(permissiveness)을 고려하지 않음
  2. 실제 응용 요구: 사이버-물리 시스템 제어에서는 추가 제약 조건과 런타임 변화에 적응하기 위해 허용적 제어기가 필요함
  3. 탄력적 제어 요구: 시스템은 장애 또는 환경 변화에 직면할 때 견고성을 유지해야 함

연구 동기

  • 기존의 전략 템플릿 개념은 확정적 게임에만 적용되며 확률적 게임에 대한 지원이 부족함
  • 무한한 수의 승리 전략을 포착할 수 있는 프레임워크가 필요하여 빠른 전략 적응을 지원함
  • CPS 제어 등 실제 응용에서 허용성과 탄력성은 핵심 요구 사항임

핵심 기여

  1. 거의 확실한 승리 전략 템플릿 알고리즘: 다섯 가지 승리 목표(안전성, 도달성, Büchi, co-Büchi, 패리티)에 대한 거의 확실한 승리 전략 템플릿 구성 알고리즘 제시
  2. 양의 확률 승리 전략 템플릿: 양의 확률 승리 기준 하에서의 전략 템플릿 구성 및 조합 알고리즘 개발
  3. 전략 템플릿 비교 프레임워크: 허용성 및 크기를 기반으로 한 템플릿 비교 논의 제공
  4. 전략 추출 방법: 주어진 템플릿에서 승리 전략을 추출하는 새로운 방법 제시, 승리 목표와 허용성의 균형 조정

방법론 상세 설명

작업 정의

확률적 게임 정의: G = (V, E, (V□, V○, V△)), 여기서:

  • V는 정점 집합, E는 간선 집합
  • V□, V○, V△는 각각 Even 플레이어, Odd 플레이어, Random 플레이어의 정점
  • "2.5" 플레이어 게임이라고 불리며 두 명의 주요 플레이어와 하나의 무작위 플레이어를 포함

전략 템플릿 정의: T = (P, L, C), 여기서:

  • P ⊆ E□는 비활성화된 간선 집합
  • L ⊆ 2^E□는 활성 그룹 집합
  • C ⊆ E□는 공동 활성 간선 집합

모델 아키텍처

1. 거의 확실한 승리 전략 템플릿 구성

안전성 목표(G X):

SafetyTemplate(G, X):
1. W□ ← νY.(X ∩ (Pre□(Y) ∪ Pre(Y)))
2. P ← Edges□(W□, V \ W□)
3. return (P, ∅, ∅)

도달성 목표(F X):

ReachabilityTemplate(G, X):
1. A ← Attr'(X)
2. W□ ← Attr'□(A)
3. P ← Edges□(W□, V \ W□)
4. C ← Edges□(W□ \ A, W□ \ A)
5. return (P, ∅, C)

Büchi 목표(GF X): LiveGroups 함수를 통해 활성 그룹을 구성하여 경로가 목표 집합을 무한히 방문하도록 보장.

패리티 목표:

  1. 확률적 게임을 확정적 게임으로 축약(Reduce 알고리즘 사용)
  2. 확정적 게임의 전략 템플릿 구성
  3. 확률적 게임의 템플릿으로 변환

2. 양의 확률 승리 전략 템플릿 구성

PositiveTemplate(G, φ):
1. W□, W○ 및 거의 확실한 승리 템플릿 T^(a) 계산
2. W? ← V \ (W□ ∪ W○)
3. P^(p) ← P^(a) ∪ Edges□(W?, W○)
4. C^(p) ← C^(a) ∪ Edges□(W?, W?)
5. return T^(p) = (P^(p), L^(p), C^(p))

기술 혁신 포인트

  1. 집합 연산 확장: Random 플레이어를 고려한 새로운 집합 연산자 도입(예: Pre△(X', X), Attr'□(X))
  2. 템플릿 조합 알고리즘: 템플릿 충돌 감지 메커니즘 제시, 충돌 시 재계산
  3. 매개변수화된 전략 추출: 매개변수 α 및 β를 사용하여 허용성과 목표 달성 속도의 균형 조정
  4. 양의 확률 승리 확장: 양의 확률 승리 기준에 전략 템플릿을 확장한 최초 연구

실험 설정

이론적 검증

논문은 주로 이론적 증명을 통해 알고리즘의 정확성을 검증하며, 다음을 포함:

  • 각 템플릿 구성 알고리즘의 정확성 정리
  • 전략 추출 방법의 허용성 정리
  • 템플릿 조합 알고리즘의 정확성 증명

복잡도 분석

  • 전략 구성 알고리즘의 최악의 경우 실행 시간은 표준 알고리즘과 일치
  • 템플릿 조합 및 전략 추출은 런타임에 효율적으로 실행 가능

실험 결과

이론적 결과

정리 10-14: 각 승리 목표의 전략 템플릿 구성 알고리즘의 정확성 증명

  • SafetyTemplate이 구성한 템플릿은 G X에 대해 거의 확실한 승리
  • ReachabilityTemplate이 구성한 템플릿은 F X에 대해 거의 확실한 승리
  • 다른 목표에도 유사하게 적용

정리 18: PositiveTemplate이 구성한 템플릿은 거의 확실한 승리와 양의 확률 승리 모두에 해당

정리 27: 매개변수화된 추출 방법은 원래 Extract 방법보다 더 허용적

허용성 분석

명제 22: P ⊇ P', L ⊇ L', C ⊇ C'이면 T는 T'보다 더 허용적이지 않음

명제 23: T가 T'보다 더 허용적이지 않고 T'이 승리하면 T도 승리함

실제 응용 가능성

논문은 확정적 게임 기반 실험 결과에 따르면 전략 템플릿이 증분 합성에서 최소 2배의 가속을 달성할 수 있으며, 용장 제어에서 30%의 선택이 비활성화되어도 재계산을 효과적으로 감소시킬 수 있음을 지적한다.

관련 연구

고전적 허용성 이론

  • Ramadge와 Wonham (1987)이 감독 제어에서 허용성 개념을 공식적으로 도입
  • Bernet 등이 패리티 게임에서 최대 허용 전략의 존재성 증명

전략 템플릿 발전

  • Anand 등이 TACAS 및 CAV 2023에서 확정적 게임의 전략 템플릿 도입
  • 본 연구는 확률적 게임으로 전략 템플릿을 확장한 최초 연구

확률적 게임 해결

  • Chatterjee 등의 확률적 패리티 게임 축약 방법
  • Banerjee 등의 확률적 게임을 위한 집합 연산자

결론 및 논의

주요 결론

  1. 전략 템플릿 개념을 확정적 게임에서 확률적 게임으로 성공적으로 확장
  2. 두 가지 승리 기준과 다섯 가지 승리 목표를 포괄하는 완전한 알고리즘 프레임워크 제공
  3. 새로운 전략 추출 방법은 정확성을 보장하면서 허용성 향상

한계

  1. 양의 확률 승리 전략은 최적 확률을 보장하지 않음
  2. 알고리즘 구현 및 실험 검증이 필요함
  3. 유한 상태 게임만 고려

향후 방향

  1. 동일한 허용성을 유지하면서 더 작은 템플릿 구성
  2. 측정 시간 논리(MTL) 공식으로 정의된 목표로 확장
  3. 실시간 시스템에 적용

심층 평가

장점

  1. 이론적 기여 상당함: 전략 템플릿을 확률적 게임으로 확장한 최초 연구, 이론 프레임워크 완전함
  2. 알고리즘 설계 합리적: 기존 집합 연산 및 축약 기술을 교묘하게 활용
  3. 응용 전망 광범위: 사이버-물리 시스템 제어에 중요한 실제적 의미
  4. 수학적 엄밀성: 완전한 정확성 증명 제공

부족한 점

  1. 실험 검증 부족: 주로 이론 연구로 실제 구현 및 성능 평가 부족
  2. 최적성 문제: 양의 확률 승리 전략은 최적성을 보장하지 않음
  3. 복잡도 분석 부족: 실제 계산 복잡도에 대한 분석이 비교적 간략함

영향력

  1. 학술적 가치: 확률적 게임 이론에 새로운 도구 및 방법 제공
  2. 실용적 가치: 허용적 제어기 설계에 이론적 기초 제공
  3. 확장성: 후속 연구를 위한 좋은 기초 프레임워크 제공

적용 시나리오

  1. 사이버-물리 시스템의 견고한 제어
  2. 적응성이 필요한 자동화 시스템
  3. 다중 목표 최적화 제어 시스템 설계
  4. 용장 제어 시스템

참고 문헌

논문은 35편의 관련 문헌을 인용하며, 주로 다음을 포함:

  • 게임 이론 기초 문헌
  • 감독 제어 이론
  • 전략 템플릿 관련 연구
  • 확률적 게임 해결 알고리즘
  • 선형 시간 논리 및 모델 검증

종합 평가: 이는 고품질의 이론 연구 논문으로, 전략 템플릿 개념을 확정적 게임에서 확률적 게임으로 성공적으로 확장하여 허용적이고 탄력적인 제어를 위한 중요한 이론적 기초를 제공한다. 실험 검증이 부족하지만 이론적 기여가 상당하며 관련 분야에 중요한 추진력을 제공한다.