Event Calculus Meets Hybrid ASP

기술 요약: 이벤트 계산법과 하이브리드 ASP의 결려

문제 정의

이벤트 계산법(Event Calculus, EC)은 자연어와의 의미론적 근접성과 이산적 및 연속적 변화를 모두 모델링할 수 있는 능력 덕분에 안전 필수 사이버 물리 시스템(CPS)을 명세하는 데 적합한 논리적 형식론이다. 그러나 실제 세계의 CPS 명세를 다룰 때 연속적인 변화와 시간 및 시스템 속성(fluents)의 크거나 조밀한 값 도메인을 처리하는 데 있어 상당한 어려움에 직면한다.

현재의 최첨단 ASP(Answer Set Programming) 기반 추론 도구들은 다음과 같은 요구 사항을 충족하는 데 어려움을 겪고 있다:

1. 그라운딩 기반 솔버 (예: clingo): 밀집된 도메인의 이산화(discretization)를 요구한다. 정밀도(예: 초 단위에서 밀리초 단위로)를 높이면 표현상의 부정확성을 완화할 수 있지만, 이는 그라운드 프로그램의 크기에 대한 조합 폭발(combinatorial explosion)을 초래하여 솔버가 메모리 부족이나 시간 초과 문제를 겪게 만든다.
2. 그라운딩 프리 솔버 (예: s(CASP)): 이러한 이산화 과정을 피하고 그라운딩 폭발을 방지하지만, 탑다운(top-down) 실행에 의존하므로 비종료(non-termination) 문제에 취약하며 현대적인 그라운딩 기반 솔버의 최적화된 성능을 갖추지 못했다.

결과적으로, 정밀도를 희생하지 않으면서 연속적인 변화를 정확하게 모델링할 수 있는 도구 사이에 공백이 존재한다.

방법론: 하이브리드 이벤트 계산법 (Hybrid EC)

저자들은 이러한 한계를 해결하기 위해 설계된 이산 이벤트 계산법(Discrete Event Calculus, DEC)의 확장된 공리화인 **하이브리드 EC(Hybrid EC)**를 소개한다. 이 접근 방식은 표준 ASP와 정수 및 유리수에 대한 선형 제약 조건을 결합한 패러다임인 하이브리드 ASP를 활용한다.

하이브리드 EC의 핵심 기술 혁신은 다음과 같다:

1. 함수적 플루언트 (Functional Fluents)

표준 DEC가 관계형 플루언트(특정 시점에 참/거짓)를 사용하는 것과 달리, 하이브리드 EC는 함수적 플루언트를 도입한다. 이 플루언트의 값은 기호적 항(예: (F, S))으로 표현되며, 그 값은 명시적인 그라운딩이 아닌 선형 제약 조건에 의해 결정된다. 이를 통해 플루언트가 모든 가능한 값에 대해 그라운드 원자(ground atom)를 생성하지 않고도 조밀한 값을 가질 수 있게 한다.

2. 하이브리드 시간 표현

DEC는 정수 시간 단계($T, T+1$)를 기반으로 작동한다. 하이브리드 EC는 이를 시스템 진화의 순서를 나타내는 추상적 단계 인덱스($S, S+1$)로 대체한다.

• 이산 단계: 이벤트의 순서만이 이산 단계로서 그라운딩된다.
• 조밀한 시간: 각 단계와 관련된 실제 시간은 이론적 원자(theory atoms, 예: (time, S))를 통해 제약 조건 솔버에 의해 처리된다.
• 매핑: 특정 시점 $T$에서의 이벤트 관측은 제약 조건을 통해 추상적 단계 $S$로 매핑되며, 이를 통해 그라운딩 크기가 시간 도메인의 크기가 아닌 이벤트의 수에 의존하도록 보장한다.

3. 공리화 (HEC)

저자들은 함수적 플루언트와 하이브리드 시간 표현을 수용하기 위해 DEC(특히 Lee와 Palla, 2012의 방식)의 공리들을 확장하였다. 주요 수정 사항은 다음과 같다:

• 관성(Inertia) 및 이벤트 효과: 규칙들은 선형 표현(예: &sum{(F,S)} = (F,S+1))을 사용하여 함수적 플루언트의 값을 할당하도록 수정되었으며, 이는 이벤트가 새로운 값을 시작하거나 관성으로부터 플루언트를 해제하지 않는 한 유지된다.
• 연속적 변화: 궤적(Trajectories)은 이산 단계 수가 아닌 실제 단계 간의 시간 차이($R \times ((time, S_1+S_2) - (time, S_1))$)를 기준으로 플루언트 값을 계산하도록 재정의되어, 단조 선형 연속 변화를 정확하게 모델링할 수 있게 한다.
• 트리거된 이벤트: 연속적인 변화에 의해 트리거되는 이벤트(예: 지면에 닿는 것)를 처리하기 위해, 시스템은 no_jump 제약을 사용한다. 이는 단조 변화 중에 단계가 임계값(예: 높이 0)을 "건너뛰는" 것을 방지하여 트리거 조건이 정확히 충족되도록 보장한다.

4. 구현 및 솔빙

구현에는 두 가지 하이브리드 ASP 솔버가 사용된다:

• clingcon: 정수에 대한 선형 제약을 지원한다.
• clingo-lpx: 유리수에 대한 선형 제약을 지원한다.

시스템은 증분형 솔빙(incremental solving) 접근 방식을 사용한다. 최소한의 단계 수로 시작하여 모델이 발견될 때까지 단계 수를 반복적으로 늘려나간다. 이는 사용자가 적절한 단계 수를 직접 추측할 필요가 없게 만든다. 이 접근 방식은 정의된 단계 범위 내에 솔루션이 존재하는 경우 종료를 보장한다.

주요 기여

1. 하이브리드 EC 공리화: 조밀한 도메인을 그라운딩 폭발 없이 표현할 수 있도록 함수적 플루언트와 추상 단계 기반 시간 매핑을 통합한 DEC의 공식적 확장.
2. 정확한 연속 모델링: clingo-lpx와 유리수를 활용함으로써, 기존의 ASP 기반 EC 구현에서 불가능했던(이산화 아티팩트 없이) 연속적 변화(조밀한 도메인)에 대한 정확한 추론을 가능하게 함.
3. 확장성: 그라운딩 크기가 시간 및 값 도메인의 크기에서 분리되어 이벤트 수에 따라 결정됨으로써, 대규모 도메인을 효율적으로 처리할 수 있음.
4. 이중 구현: 정수(clingcon) 및 유리수(clingo-lpx) 솔버를 모두 사용하는 구현을 제공하여 접근 방식의 유연성을 입증함.

실험 결과

저자들은 문헌(예: 카운터, 낙하하는 물체, 도난당한 자동차, 열기구)에 등장하는 30개 이상의 벤치마크 문제를 통해 접근 방식을 평가하였다.

• 표현력: 하이브리드 EC 구현체(clingcon 및 clingo-lpx)는 표준 clingo(DEC) 구현체가 처리한 모든 문제를 성공적으로 해결하였다. 또한, clingo-lpx는 clingo와 clingcon이 정확하게 처리할 수 없었던 연속적 변화(조밀한 도메인)가 필요한 문제들을 성공적으로 해결하였다.
• 확장성 (도메인 크기): 시간 및 값 도메인의 크기를 변화시키는 실험에서, clingo의 실행 시간은 도메인 크기가 커짐에 따라 지수적으로 증가(타임아웃 발생)하였다. 반면, clingcon과 clingo-lpx는 도메인 크기에 영향을 받지 않고 안정적인 실행 시간을 유지하였다.
• 확장성 (이벤트 수): 성능은 이벤트 수에 따라 선형적으로 확장되었으며, 이는 본 접근 방식이 도메인의 크기가 아닌 이벤트의 수에 의해 구동됨을 확인시켜 준다.
• 유리수 vs 정수: 유리수를 사용하는 clingo-lpx가 정수 추론에 비해 확장성에 부정적인 영향을 미치지 않으면서도, 연속 모델링에 필요한 정밀도를 제공하였다.

의의 및 주장

본 논문은 하이브리드 EC가 이벤트 계산법의 의미론적 풍부함과 현재 ASP 솔버의 계산적 한계 사이의 간극을 성공적으로 메웠다고 주장한다.

• 정확성: 이산화로 인한 부정확성을 제거하여 연속적인 물리적 프로세스를 충실하게 모델링할 수 있게 한다.
• 효율성: 대규모 또는 조밀한 도메인과 관련된 그라운딩 폭발을 방지하여, 복잡한 CPS 명세에 대한 엄격한 검증을 가능하게 한다.
• 종료성: 그라운딩 프리 쿼리 구동 방식과 달리, 하이브리드 ASP 접근 방식은 솔루션이 존재하는 인스턴스에 대해 종료를 보장한다.

저자들은 현재 구현이 단조 선형 변화를 처리하지만, 조밀한 시간 추론은 제노(Zeno) 현상과 같은 과제를 안겨준다고 언급하였다. 이와 관련된 문제들에 대한 인코딩을 제공하기는 했으나, HEC 맥락에서 이러한 특정 현상을 다루는 것은 향후 연구 과제로 남겨두었다. 본 연구는 연속 역학을 가진 안전 필수 시스템을 추론하기 위해 하이브리드 ASP를 사용하는 기초를 마련하였다.