기술 요약: LTL 작업을 수행하는 다중 에이전트 시스템의 보안 인식 계획 및 제어

문제 정의

본 논문은 선형 시간 논리 (LTL) 명세 하에서 연속 작업 공간에서 작동하는 다중 에이전트 시스템 (MAS) 의 계획 및 제어 과제를 다루며, 동시에 수동 침입자에 대한 정보 보안을 보장하는 문제를 해결합니다.

기존의 LTL 기반 계획 방법은 이산 계획을 합성하기 위해 연속 동역학을 유한 상태 모델로 추상화한 후, 이를 연속 궤적으로 정제합니다. 그러나 이러한 접근법은 일반적으로 정보 보안을 간과합니다. 드론 스웜이나 지능형 교통 시스템과 같은 중요한 응용 분야에서는 작업의 정확성과 기밀성 사이의 균형이 필수적입니다. 구체적인 문제는 선형 아핀 동역학을 가진 에이전트에 대한 제어기를 합성하여, 결과적으로 생성된 연속 궤적이 전역 LTL 작업을 만족하면서도 부분적인 에이전트 위치 관측을 가진 악의적 관찰자가 다음 두 가지를 추론하지 못하도록 하는 것입니다:

1. "비밀" 작업 (지정된 비밀 영역 방문) 이 실행되었는지 여부.
2. 해당 비밀 작업을 수행한 특정 에이전트가 누구인지.

저자들은 단일 에이전트 시스템과 일부 이산 다중 에이전트 시스템에 대해서는 기반을 둔 보안 (opacity-based security) 이 탐구되었으나, 연속 동역학, 입력 제약, 그리고 복잡한 LTL 명세를 동시에 처리하는 시스템에 대해서는 격차가 존재한다고 지적합니다.

방법론

제안된 프레임워크는 보안 제약 조건을 합성 절차에 직접 통합하는 "구축 시 보안 (secure-by-construction)" 접근 방식을 따릅니다. 방법론은 네 가지 주요 단계로 진행됩니다:

1. 추상화 및 보안 모델링

• 시스템 모델: 작업 공간은 겹치지 않는 다면체 (polytopes) 로 분할됩니다. 에이전트 동역학은 가중 전이 시스템 (WTS) 으로 추상화됩니다. 개별 에이전트 WTS 의 동기적 곱을 통해 전역 WTS(gWTS) 가 형성됩니다.
• 보안 정의: 침입자의 관측 능력 ($H_i$) 에 기반하여 두 가지 상호 보완적인 보안 개념이 도입됩니다:
  • A 형 보안: 침입자가 어떤 에이전트가 비밀 상태를 방문했는지 추론하지 못하도록 방지합니다. 이는 비밀 방문이 발생하는 모든 "실제" 경로에 대해, 동일한 관측을 가지면서 에이전트가 비비밀 상태를 방문하는 구별 불가능한 "복제" 경로가 존재하도록 보장함으로써 달성됩니다.
  • B 형 보안: 침입자가 비밀 상태를 방문한 어떤 에이전트인지 식별하지 못하도록 방지합니다. 이는 에이전트 $i$가 비밀 상태를 방문할 때, 해당 시간 단계에서 최소 한 명의 다른 에이전트 $k$가 동일한 관측을 생성해야 함을 요구합니다.
• 보안 추상화: 이러한 속성을 강제하기 위해 저자들은 다음을 구성합니다:
  • Twin-gWTS: 구별 불가능한 전역 상태 쌍을 포착하는 곱 시스템.
  • Secure Twin-gWTS: 실제 에이전트와 복제 에이전트가 동시에 비밀 상태에 있는 상태 쌍을 제거한 Twin-gWTS 의 정제 버전.
  • Type-B gWTS: 비밀 방문이 다른 에이전트의 관측에 의해 "가려지도록" 보장하는 전역 상태 공간의 제한.

2. 전이 실현 가능성 검증

LTL 합성을 적용하기 전에, 프레임워크는 보안 추상화 내의 이산 전이가 연속 작업 공간에서 동역학적으로 실현 가능한지 검증합니다.

• 제어 장벽 함수 (CBF): 저자들은 에이전트가 할당된 다면체 내에 머무르도록 보장 (전진 불변성) 하고 특정 시간에 경계를 횡단하도록 보장하기 위해 CBF 를 사용합니다.
• 2 차 계획법 (QP): 각 이산 전이에 대해, 에이전트를 영역 중심점 사이로 이동시키면서 동역학, 입력 한계, CBF 제약을 만족시키는 제어 입력을 찾기 위해 중앙 집중식 QP 가 해결됩니다. 해가 존재하지 않으면 해당 전이는 추상 모델에서 폐기됩니다.

3. LTL 합성

• 곱 Büchi 자동기 (PBA): 보안 gWTS 는 LTL 명세에서 유도된 비결정적 Büchi 자동기 (NBA) 와 동기화됩니다.
• 경로 탐색: 알고리즘은 비용 함수 (접두어 비용과 접미사 비용의 균형) 를 최소화하는 접두어 - 접미사 경로를 PBA 에서 탐색합니다. 이 경로는 LTL 작업과 보안 제약 조건을 모두 만족하는 이산 계획을 나타냅니다.

4. 연속 궤도 생성

최적의 이산 경로는 QP 단계에서 계산된 실현 가능한 궤도 세그먼트들을 연결하여 연속 궤도로 정제됩니다. 결과적으로 생성된 연속 궤도가 LTL 공식과 보안 속성을 만족한다는 형식적 보장이 제공됩니다.

주요 기여

본 논문은 다음과 같은 기여를 주장합니다:

1. 새로운 보안 개념: 다중 에이전트 시스템을 위한 A 형 및 B 형 보안의 도입으로, 기존 오페시티 (opacity) 정의를 완화하여 확장성을 개선하면서도 강력한 보안 보장 (합리적 부인 가능성 및 에이전트 익명성) 을 유지합니다.
2. 연속 동역학 프레임워크: 연속 아핀 동역학 및 입력 제약을 가진 다중 에이전트 시스템에 직접 적용 가능한 계획 프레임워크입니다. 저자들은 기존 연구가 유한 상태 모델에 집중했던 반면, 이는 알려진 바에 따르면 이러한 보안 제약 조건과 함께 일반적인 LTL 작업을 처리하는 최초의 프레임워크라고 주장합니다.
3. 복잡도 감소: 제안된 이산 계획 알고리즘은 기존 다중 에이전트 보안 인식 방법보다 계산 복잡도가 현저히 낮습니다 (특히 검색 공간에 대해 $(2|Q|)^{2M^2+M}$ 상태에서 $|Q|^{2M}$ 상태로 감소).

결과 및 사례 연구

본 프레임워크는 두 대의 드론을 포함하는 사례 연구를 통해 검증되었습니다:

• 시나리오: 드론 1 은 공기 질을 스캔하고 데이터를 인코딩하며, 드론 2 는 데이터를 중계하고 진단 스테이션을 방문합니다. 두 드론 모두 장애물 영역을 피해야 합니다.
• 작업: 장애물을 피하면서 스캔, 인코딩, 전송의 반복 시퀀스와 eventual inspection 을 요구하는 LTL 공식.
• 보안: 두 영역 (민감 데이터 수집 및 진단 스테이션) 이 비밀로 지정됩니다. 시스템은 드론의 일반 위치 (북부/남부 구역) 를 관측하는 침입자에 대해 A 형/B 형 보안을 만족해야 합니다.
• 결과: 알고리즘은 다음과 같은 궤도를 성공적으로 합성했습니다:
  • 드론 1 이 비밀 영역을 방문할 때, 동일한 관측을 가진 비비밀 영역에 있는 "복제" 경로가 표시됩니다 (A 형 충족).
  • 드론 2 는 비밀 방문 동안 드론 1 과 동일한 관측을 생성하도록 배치되어, 침입자가 책임 있는 에이전트를 식별하지 못하게 합니다 (B 형 충족).
• 성능: 전체 알고리즘 (추상화, QP 해결, 경로 탐색 포함) 은 MacBook Air M2 에서 약 70 초에 실행되었습니다.

중요성 및 주장

본 논문은 자율 사이버 - 물리 시스템을 위한 구축 시 보안 (secure-by-construction) 전략을 향한 중요한 진전으로 자신의 작업을 위치시킵니다. 저자들은 보안 제약 조건을 LTL 합성 절차에 직접 통합함으로써, 결과적인 행동이 전역 임무 명세와 기밀성 요구 사항을 모두 만족한다는 형식적 보장을 제공한다고 주장합니다.

이러한 중요성은 보안 인식 방식으로 고수준 논리적 계획과 저수준 연속 제어 사이의 격차를 해소하는 데 있습니다. 저자들은 그들의 접근 방식이 보안 인식 LTL 합성 컨텍스트 내에서 연속 동역학과 입력 제약을 직접 처리하는 최초의 방법이며, 계산 복잡도 측면에서 기존 이산 전용 방법보다 우수한 확장 가능한 솔루션을 제공한다고 강조합니다.

본 논문은 겸손하게 결론을 내리며, 향후 연구는 비선형 동역학으로 프레임워크를 확장하고 대규모 다중 에이전트 시스템의 확장성을 더욱 개선하기 위해 계층적 아키텍처를 조사할 수 있음을 언급합니다.