기술 요약: RDFdL – RDF와 미분 동적 논리(Differential Dynamic Logic)의 통합

1. 문제 정의

사이버-물리 시스템(CPS)과 산업용 디지털 트윈은 정적 구조 지식(예: 장치 계층 구조, 유지보수 책임, 센서 메타데이터)과 동적 행동 지식(예: 상미분 방정식(ODE)에 의해 제어되는 연속적인 진화)의 통합을 필요로 한다.

현재의 시맨틱 웹 기술(RDF, RDFS, OWL, SHACL, SPARQL)은 정적 그래프 데이터를 표현하고, 스키마를 검증하며, 구조적 관계를 쿼리하는 데 탁월하다. 그러나 이러한 기술들은 연속적인 역학, 도달 가능성(reachability), 또는 미분 방정식으로 기술된 시스템의 안전성 속성을 추론할 수 있는 형식적 의미론(formal semantics)이 부족하다. 반대로, KeYmaera X와 같은 미분 동적 논리(dL) 기반의 형식 검증 도구들은 하이브리드 시스템에 대한 안전성 및 도달 가능성을 엄격하게 증명할 수 있지만, 풍부한 메타데이터, 프로비넌스(provenance), 그래프 쿼리 기능으로부터 고립되어 운영된다.

본 연구가 다루는 핵심 문제는 동적인, 형식적으로 검증된 행동(예: "상태 A에서 상태 B로의 안전한 전이가 가능한가?")을 정적 메타데이터(예: "이 전이에 연관된 장치의 담당 기술자는 누구인가?")와 단일 쿼리 프레임워크 내에서 함께 쿼리할 수 없다는 점이다. 기존 도구들은 그래프 기반의 구조적 추론과 정리 증명기(theorem-prover) 기반의 동적 검증 사이의 간극을 메우지 못하고 있다.

2. 방법론: RDFdL 프레임워크

저자들은 정적 지식 그래프와 형식적 하이브리드 시스템 검증 사이에 견고한 가교를 만들기 위해 RDF와 미분 동적 논리(dL)를 통합하는 프레임워크인 RDFdL을 제안한다. 이 접근 방식은 검증된 동적 전이를 RDF 그래프 내의 함의된(entailed) 트리플로 취급하여 SPARQL로 쿼리할 수 있게 한다.

2.1 데이터 모델링 및 표현

• 하이브리드 시스템 추상화: 시스템은 상징적 **상태 영역(state regions)**의 집합으로 모델링된다. 상태 영역은 연속 변수(예: 온도 범위)에 대한 수학적 조건과 이산 모드(예: On/Off)를 나타내는 RDF 리소스이다.
• 상태 정의를 위한 SHACL: SHACL 셰이프(shapes)는 이러한 상태 영역의 수치적 경계와 모드 제약 조건을 정의하는 데 사용된다. SHACL은 실시간 관측값을 이러한 셰이프에 따라 검증하여 현재의 상징적 영역을 식별하지만, 역학 자체를 정의하지는 않는다.
• ODE 통합: 장치 모드는 RDF 내의 ODE 레코드와 연결된다. 각 ModeRecord는 장치, 특정 모드, 그리고 해당 모드에서의 연속적 진화를 지배하는 ODE(도함수, 진화 도메인 제약 조건, 시작/종료 조건 포함)를 연관시킨다.
• 온톨로지: 커스텀 어휘(rdfdl)는 ModeRecord, ODE, Variable 클래스를 정의하고 장치를 역학에 연결하는 속성을 정의한다. 이 어휘는 가능한 경우 기존 표준(SSN, SOSA, PROV, schema.org)을 재사용한다.

2.2 검증 파이프라인

핵심 혁신은 dL 정리 증명기(KeYmaera X)를 RDF 추론 엔진(Apache Jena)에 직접 임베딩하는 것이다.

1. 추출(Extraction): 그래프 내의 두 상태 영역($s_1 \to s_2$) 사이의 모든 후보 전이에 대해 다음을 추출한다:
   • 전제 조건 ($\phi_1$): $s_1$의 SHACL 셰이프로부터 유도됨.
   • 후속 조건 ($\phi_2$): $s_2$의 SHACL 셰이프로부터 유도됨.
   • 하이브리드 프로그램 ($\alpha$): 공유된 모드와 관련된 ODE 레코드(연속 전이의 경우) 또는 가드 조건(이산 모드 전환의 경우)으로부터 유도됨.
2. 증명 의무 생성(Proof Obligation Generation):
   • 연속 전이 (:next): 도달 가능성(liveness property)을 검증하기 위해, 시스템은 안전성 스타일의 box 공식에 대한 반박 가능성(refutability) 의무를 생성한다. $\phi_1 \to \langle \alpha \rangle \phi_2$를 직접 증명하는 대신(KeYmaera X가 이를 잘 처리하지 못하므로), $[\alpha \& (\phi_1 \lor \phi_2)] \phi_1$을 반박하려고 시도한다. 이 공식이 반박 가능하다면, 이는 $\phi_1$에서 시작하여 $\phi_1$과 $\phi_2$의 합집합 내에 머물며 $\phi_2$로 나가는 궤적이 존재함을 의미한다.
   • 이산 전이 (:modeChange): 시스템은 새로운 모드의 가드 조건이 소스 영역에 의해 충족되는지, 그리고 이전 모드의 종료 조건이 새로운 모드의 시작 조건과 일치하는지 검증한다.
3. 추론으로서의 함의(Inference as Entailment): Jena 규칙 엔진은 REST 인터페이스를 통해 KeYmaera X를 호출한다. 증명 의무가 해소(검증되거나 필요한 대로 반박)되면, 전이 술어(:next 또는 :modeChange)가 추론된다.
4. 결과 구체화(Result Materialization): 검증된 전이는 **함의된 트리플(entailed triples)**이 된다. 이는 선언된 트리플과 구별되지 않으며, 속성 경로 쿼리(property-path queries)를 통해 검증된 동적 경로를 정적 메타데이터 링크와 함께 탐색할 수 있게 한다.

3. 주요 기여

1. RDF 기반 하이브리드 시스템 표현: 연속 역학(ODEs)과 상태 정의(SHACL)를 RDF 그래프 내에 표현하는 공식적인 방법을 제시하여, 정적 데이터와 동적 데이터를 위한 통합된 모델을 생성한다.
2. 자동화된 dL 증명 의무 생성: RDF/SHACL 표현을 dL 공식으로 변환하는 파이프라인을 구축하며, 특히 liveness(도달 가능성) 목표를 KeY-maera X와 호환 가능한 반박 가능한 안전성 공식으로 적응시킨다.
3. RDFdL 프레임워크: 검증 결과를 논리적 함의로 취급하는 Apache Jena 및 KeYmaera X를 사용한 작동하는 구현체를 제공한다. 이를 통해 SPARQL 쿼리는 정적 메타데이터와 형식적으로 검증된 동적 행동(예: 검증된 전이의 "해피 패스"를 찾고 각 단계의 담당 기술자를 검색하는 것)에 의존하는 답변을 반환할 수 있다.
4. 건전성 보장(Soundness Guarantees): 모든 함의된 전이가 검증된 하이브리드 행동에 대응함을 입증하는 정리(lemmas)를 통해 건전성을 확립하고, 검증된 경로 전반에서 글로벌 안전 불변성(global safety invariants)이 유지됨을 입증한다.

4. 평가 및 결과

프레임워크는 네 가지 케이스 스터디를 통해 평가되었다:

• Oven (오븐): 단일 장치 서모스탯 컨트롤러 (선형 ODE).
• Empty Tank (빈 탱크): 비선형, 결합된 ODE를 가진 이중 탱크 유량 시스템.
• Yogurt Production (요거트 생산): 순차적 및 병렬 모드가 있는 다중 장치 프로세스.
• Drum-Boiler (드럼 보일러): 선형화된 2D ODE를 가진 산업용 증기 생성 시스템.

주요 결과:

• 확장성: 선형 및 다항식 역학의 경우, 증명 의무의 수는 상태 및 모드의 수에 따라 거의 선형적으로 증가한다.
• 비선형 처리: 프레임워크는 KeYmaera X가 실수 대수적 인증(이중 지수 복잡도를 가진 결정 절차)으로 전환하는 비선형 Tank 시스템을 성공적으로 처리하였으며, 이는 2D 비선형 흐름에 대한 견고성을 입증한다.
• 정확성: 모든 케이스 스터디는 증명 의무를 성공적으로 해소하였으며 글로벌 안전 불변성(예: 온도 범위)을 유지하였다.
• 런타임 검증: SHACL이 유효하지 않은 실시간 상태를 효과적으로 필터링하여, 후속 전이 추론에 유효한 상징적 영역만 사용되도록 보장함을 보여주었다.

5. 의의 및 주장

본 논문은 AI 기반 사이버-물리 시스템의 결정적 격차, 즉 동적인, 형식적으로 검증된 행동을 정적 메타데이터와 단일한 방식으로 쿼리할 수 없는 문제를 해결한다고 주장한다.

• 독특한 통합: RDF와 dL을 그들의 공통 기반인 1차 논리(first-order logic)를 통해 연결함으로써, RDFdL은 검증 결과(안전성 및 도달 가능성)를 SPARQL 쿼리에 대한 함의로 만든다.
• 실질적 적용 가능성: 이 프레임워크를 통해 엔지니어들은 "상태 A에서 B로 가는 검증된 안전한 경로가 있는가? 그리고 그 경로의 장치들에 대한 담당자는 누구인가?"와 같이 이전에는 불가능했던 복잡한 질문을 던질 수 있다.
• 제한적 범위: 저자들은 RDFdL이 하이브리드 시스템 정리 증명기나 RDF 추론 엔진을 대체하는 것이 아니라, 건전한 가교를 구축하는 것임을 명시한다. 이 접근 방식은 건전하지만 불완전하다(일반적인 하이브리드 시스템의 결정 불가능성과 증명기의 자원 제한으로 인해). 즉, 검증된 트리플이 없다는 것이 행동의 부재를 증명하는 것이 아니라, 주어진 제약 조건 내에서 증명되지 않았음을 의미한다.

이 연구는 형식 검증이 시맨틱 웹 스택에 통합될 수 있음을 보여주며, 동적 속성이 단순한 시뮬레이션이 아닌 수학적으로 증명되고 쿼리 가능한 "검증 가능한 지식 그래프"를 가능하게 한다.