로봇 안전 · 형식 검증

Predictive Varanus: 로봇 실행의 적합성 검사와 미래 결과 예측을 결합한 검증

Predictive Varanus: Combining CSP Conformance Monitoring with Predictive LTL Runtime Verification

Angelo Ferrando 외최초 공개 2026-09-15

초록과 본문 전체 89개 문단을 한국어로 번역했습니다. 그림 1개, 표 3개, 별도 수식 24개와 참고문헌 19개를 포함합니다. 원문에는 부록이 없습니다. 수식과 그림 내부 표기는 원형을 보존하고 캡션·표 머리글을 한국어로 옮겼습니다. 로봇노드 AI의 비공식 번역입니다.

저자: Angelo Ferrando(이탈리아 모데나 레조에밀리아 대학교), Matt Luckcuck(영국 노팅엄 대학교), Pedro Ribeiro(영국 요크 대학교).

초록

런타임 검증은 실행 중 실제로 관찰되는 행동을 검사하므로 자율 시스템과 로봇에 적합하다. 그러나 대개 사후 반응 방식이라는 한계가 있다. 시스템이 잘못된 이벤트를 이미 수행한 뒤에야 위반을 발견하기 때문에, 실패의 비용이나 위험이 큰 분야에서는 너무 늦을 수 있다. 본 논문은 프로세스 대수 CSP(Communicating Sequential Processes)로 작성한 모델을 사용하는 런타임 검증기 Varanus와 선형 시간 논리(LTL)의 예측적 런타임 검증을 결합한 2단계 처리 과정인 Predictive Varanus를 제시한다. 먼저 CSP 모델로 관찰된 이벤트 이력의 적합성을 검사한다. 같은 모델을 뷔히 오토마톤으로 변환하여 예측적 LTL 모니터가 탐색할 미래를 제한한다. 모델 밖의 행동은 즉시 거부하고, 모델에 맞는 현재까지의 이력은 시간적 속성의 만족을 이미 보장하는지, 위반을 이미 강제하는지, 아직 결론을 내릴 수 없는지 분류한다. 통합 모니터를 형식화하고 구현을 설명하며 핵폐기물 저장소를 검사하는 로버 사례에 적용한다. 이 사례는 기존 설계 단계의 CSP 모델을 재사용하면서, CSP 적합성 검사와 예측적 LTL을 결합해 일반 런타임 모니터보다 일찍 판정을 내릴 수 있음을 보여준다.

I. 서론

자율 로봇은 설계 시점에 일부만 알려진 환경에서 자주 동작한다. 따라서 오프라인 분석과 설계 단계 검증만으로는 충분하지 않을 수 있다. 설계 모델의 가정이 실행 중 깨지거나, 센서가 예상 밖 상황에 노출되거나, 환경과의 상호작용으로 시험하지 않은 행동에 들어갈 수 있기 때문이다. 런타임 검증(RV)은 분석 대상 시스템(SUA)이 생성하는 이벤트 이력을 의도된 행동의 형식 명세와 비교해 이러한 간극을 메운다[1,2]. 이 형식 명세를 오라클, 즉 판정 기준이라고 부른다. 로봇 분야에서는 구성요소의 소스 코드나 내부 상태에 접근하지 않고도 실행 중 명세를 준수하는지 온라인으로 보증할 수 있어 특히 유용하다[3].

일반 RV는 반응적이다. 행동을 강제하거나 피해를 줄이는 기능과 결합하지 않으면, 관련 이벤트를 관찰한 뒤에만 위반을 보고한다. 예측적 런타임 검증(PRV)은 대상 시스템 모델을 이용해 현재 이력 뒤에 가능한 연속 실행을 살펴보고, 특정 속성이 반드시 만족되거나 반드시 위반되는지 검사한다[4,5,6]. 판정은 모델을 전제로 한다. 모델에 없는 임의의 고장을 예측하는 것이 아니라, 모델에 부합하는 결과인 불가피한 임무 중단, 검사 지점 방문 실패 또는 보장된 완료를 미리 판단한다.

연구진의 최근 연구는 CSP[8] 모델을 오라클로 사용하는 RV 도구 Varanus[7]를 소개했다. Varanus는 CSP 모델이 올바른 행동을 결정론적으로 표현한다고 가정하지만 그 외의 수정을 요구하지 않는다. 따라서 FDR[9]이나 RoboChart[10] 등으로 설계 단계에서 이미 분석한 모델을 재사용할 수 있다. CSP는 이벤트 순서·동기화·통신 구조를 자연스럽게 표현하고, 많은 로봇 명세도 이러한 추상화 수준에서 작성되므로 자율 시스템 모니터링에 유용하다. 그러나 Varanus는 예측적 모니터가 아니라 반응적 모니터다. 유효하지 않은 이벤트를 관찰해야만 대상 시스템이 잘못 동작한다고 결론 내릴 수 있다.

본 논문은 Varanus와 PRV에 관한 기존 연구를 결합한 Predictive Varanus 처리 과정을 제시한다. Varanus로 CSP 적합성을 먼저 검사하고, 현재 이력과 양립하는 미래에 LTL 속성의 PRV를 적용한다. 두 상황을 구분해 감지한다. 첫째는 CSP 모델에 맞지 않아 거부되는 대상 시스템의 행동이다. 둘째는 모델에는 맞지만 LTL 속성의 만족 또는 위반이 불가피하다고 결론 내릴 수 있는 행동이다.

제안 과정은 CSP 모델에서 시간 논리의 PRV를 수행하는 방법을 보여준다. CSP 모델은 두 가지로 활용된다. 첫째는 적합성 관문인 Varanus의 오라클이고, 둘째는 예측 추론에서 허용할 미래의 근원이다. 이를 위해 CSP 모델을 뷔히 오토마톤으로 변환하고 대상 시스템 이벤트를 명제로 사상한다. 본 구현의 PRV는 LTL 검사이지만, 모듈 구조이므로 필요에 따라 다른 예측 추론을 사용할 수 있다. 논문은 이 2단계 과정을 정의하고 통합 판정 함수와 모델 변환을 형식화하며 핵시설 검사 로버 사례로 평가한다.

논문의 구성은 다음과 같다. II절은 Varanus와 PRV의 배경, III절은 Predictive Varanus 처리 과정과 형식화, IV절은 사례 적용, V절은 평가, VI절은 관련 연구, VII절은 결론을 제시한다.

II. 배경

A. CSP와 Varanus

CSP는 이벤트에 참여하는 프로세스로 시스템을 모델링한다. Varanus는 CSP 오라클이 결정론적인 유한 상태 프로세스라고 가정한다. CSP의 동작 의미론은 레이블 전이 시스템(LTS)으로 표현할 수 있다. 상태는 프로세스 구성에 대응하고 간선은 관찰 가능한 이벤트로 표시한다. 프로세스의 이력은 LTS의 유한 경로다. 대상 시스템의 실행도 모델 이력과 비교할 수 있는 이벤트 이력이므로 CSP는 RV에 적합하다.

Varanus는 CSP 모델의 LTS 표현을 RV 오라클로 사용한다. 기존 Varanus에서는 현재 LTS 상태에서 가능한 이벤트를 수용하고 그렇지 않은 이벤트를 거부한다. 엄격 모드와 허용 모드가 있으며, 허용 모드는 오라클의 이벤트 집합에 없는 이벤트를 무시한다. 이는 대상 시스템이 관련 없는 이벤트도 내보낼 때 유용하다. 본 논문에서 Varanus는 적합성 관문 역할을 하며, CSP 모델에 부합하는 이벤트만 예측 구성요소로 전달한다.

이후 $P$ 를 관찰 가능한 이벤트 집합 $\Sigma_{P}$ 위의 CSP 프로세스라고 하자. $\mathcal{L}(P)$ 는 $P$ 가 허용하는 유한 이력의 집합이다. CSP의 이력 의미론은 접두부에 대해 닫혀 있으므로[8], $\sigma\in\mathcal{L}(P)$ 는 관찰된 유한 이력 $\sigma$ 가 여전히 CSP 명세와 양립함을 뜻한다.

정의 1. CSP 적합성 술어

CSP 프로세스 $P$ 가 주어질 때 적합성 술어는 다음 함수다.

G_{P}:\Sigma_{P}^{*}\rightarrow\{\mathsf{acc},\mathsf{rej}\}

이 함수는 다음과 같이 정의한다.

G_{P}(\sigma)=\begin{cases}\mathsf{acc}&\text{if }\sigma\in\mathcal{L}(P),\\ \mathsf{rej}&\text{otherwise.}\end{cases}

이 정의는 처리 과정에서 Varanus의 역할을 나타낸다. 현재 관찰한 이력이 CSP 모델의 유효한 이력인지 평가한다. 유효하여 $G_{P}=acc$ 이면 예측 구성요소가 이력을 검사한다. 이력이 거부되어 $G_{P}=rej$ 이면 대상 시스템이 유효하지 않은 이벤트를 수행한 것이므로 예측 구성요소가 필요하지 않다.

B. LTL의 예측적 런타임 검증

$\varphi$ 를 이벤트 집합 $\Sigma$ 위의 LTL 속성, $M$ 을 같은 집합 위에서 시스템 실행을 기술하는 모델이라고 하자. PRV의 유한 접두부 $\sigma$ 에 대한 판정은 $\sigma$ 가 속성 $\varphi$ 를 만족하거나 위반하는지만으로 정해지지 않는다. $M$ 이 허용하는 $\sigma$ 의 모든 연속 실행이 만족하는지, 모두 위반하는지, 둘 다 가능한지에 따라 정해진다[5,6,11].

구현에 맞춰 확정적 만족( $\top$ ), 확정적 위반( $\bot$ ), 미결정( $?$ )의 3값 논리를 사용한다. 더 풍부한 예측 의미론에서 ‘참일 가능성’과 ‘거짓일 가능성’이라는 중간 판정을 하나의 미결정 결과로 합친 형태다. 유효하지 않은 접두부는 Varanus가 거부하기 때문이다.

정의 2. 예측 판정

$M$ 을 $\Sigma$ 위의 모델, $\varphi$ 를 LTL 속성이라고 하고 다음을 정의하자.

\mathsf{Cont}_{M}(\sigma)=\{\tau\in\Sigma^{\omega}\mid\sigma\tau\in\mathcal{L}(M)\}.

그러면 모든 유한 이력 $\sigma\in\Sigma^{*}$ 에 대해 다음 함수는

\mathsf{Pred}_{\varphi,M}(\sigma)\in\{\top,\bot,?\}

아래와 같이 정의된다.

\mathsf{Pred}_{\varphi,M}(\sigma)=\begin{cases}\top&\text{if }\forall\tau\in\mathsf{Cont}_{M}(\sigma).\ \sigma\tau\models\varphi,\\ \bot&\text{if }\forall\tau\in\mathsf{Cont}_{M}(\sigma).\ \sigma\tau\not\models\varphi,\\ ?&\text{otherwise.}\end{cases}

표준 LTL 의미론을 사용할 수 있도록 유한 이력 뒤에 skip 명제가 무한히 반복되는 접미부를 붙인다. 대상 시스템이 만든 이력의 이벤트는 $\neg\texttt{skip}$ 을 만족하고, 이력이 종료된 뒤 skip이 무한히 이어진다. CSP에서는 skip 이벤트의 무한한 연속 실행에 해당한다.

III. Predictive Varanus

그림 1은 Predictive Varanus의 구성요소다. 대상 시스템이 이벤트 이력을 내보내면 Varanus가 각 이벤트를 CSP 모델과 비교해 유효성을 검사한다. 유효한 이벤트는 예측적 LTL 모니터로 전달된다. 예측 모니터는 이벤트를 명제 집합으로 사상하고 CSP 모델에서 변환한 뷔히 오토마톤으로 PRV를 수행한다. 따라서 Varanus가 이미 무효로 거부한 이벤트의 미래를 예측 구성요소가 추론하지 않는다.

그림 1. Predictive Varanus 검증 과정. 같은 CSP 모델을 Varanus의 실행 중 적합성 관문과 예측적 LTL 모니터가 사용하는 뷔히 오토마톤의 근원으로 재사용한다.

A. CSP에서 명제 기반 모델로

CSP 모델을 명제 수준 런타임 검증으로 변환하는 접근은 이미 존재한다. 대표적으로 CSP 정규화 그래프를 크립키 구조로 변환하여 이력과 거부 집합을 건전하게 런타임 검증하는 방법이 있다[12]. 본 구성의 목적은 다르다. 안전성 검사를 목표로 삼는 대신, CSP 모델이 수용한 이벤트의 미래에 대해 예측적 LTL 모니터링을 수행할 명제 기반 $\omega$ -오토마톤을 도출한다.

CSP에서 예측 모델로

$P$ 를 유한 상태 CSP 프로세스라고 하자. 첫 단계는 $P$ 의 표준 동작 의미론이 유도하는 유한 LTS를 추출하는 것이다. 형식적으로 다음과 같이 쓴다.

\mathcal{T}(P)=(S,s_{0},\Sigma_{P},\rightarrow),

여기서 $S$ 는 $P$ 의 도달 가능한 잔여 상태 집합, $s_{0}\in S$ 는 초기 상태, $\Sigma_{P}$ 는 $P$ 의 이벤트 집합이며, 다음은

\rightarrow\;\subseteq S\times\Sigma_{P}\times S

전이 관계다. $s,s^{\prime}\in S$ 이고 $a\in\Sigma_{P}$ 일 때 다음 전이는

s\xrightarrow{a}s^{\prime}

표준 CSP 동작 의미론에 따라 프로세스가 이벤트 $a$ 를 수행하여 상태 $s$ 에서 상태 $s^{\prime}$ 로 바뀔 수 있을 때 성립한다.

직관적으로 $\mathcal{T}(P)$ 의 각 상태는 어떤 유한 실행 뒤 프로세스에 남은 행동을 나타내고, 레이블이 있는 전이는 다음에 가능한 이벤트를 기록한다. $P$ 가 유한 상태이므로 전이 시스템도 유한하다. 구현에서 Varanus는 CSP 구문 분석과 상태 공간 생성을 FDR에 맡겨 이 구조를 얻고, 도달 가능한 전이 시스템을 실행 중 사용할 수 있도록 명시적으로 구성한다. 따라서 모니터가 사용하는 전이 시스템은 임의로 만든 구현 산출물이 아니라 CSP 표준 의미론의 명시적인 유한 상태 표현이다.

CSP 모델과 예측적 LTL 계층을 연결하기 위해 $\mathcal{T}(P)$ 에서 Hanoi Omega-Automata(HOA) 형식으로 인코딩한 $\omega$ -오토마톤을 도출한다.

\mathcal{B}_{P}=(S,s_{0},2^{\mathit{AP}},\delta,F_{P}),

여기서 다음이 성립하며,

\mathit{AP}=\{\pi(a)\mid a\in\Sigma_{P}\}\cup\{\texttt{skip}\}

$F_{P}=S$ 이므로 모든 상태가 수용 상태다. 이는 오토마톤 기반 시간 논리 검증에서 크립키 구조를 사용하는 표준 방식과 유사하다. LTL은 무한 행동을 대상으로 해석하므로 종료 상태 뒤에는 같은 상태가 무한히 반복되는 접미부가 필요하다. 본 설정에서는 모든 종료 상태에 skip 자기 루프를 추가한다. 결과적으로 CSP 모델의 모든 극대 유한 실행이 무한 단어를 유도하며, $\mathcal{B}_{P}$ 는 이 종료 후 반복 규칙에 따라 CSP 모델 행동에서 얻은 무한 연속 실행을 정확히 수용한다. 사상 $\pi$ 는 각 관찰 가능한 CSP 이벤트에 새로운 원자 명제를 대응시키고, skip은 종료 이후의 접미부용으로 남겨둔다.

모든 CSP 전이에 대해,

s\xrightarrow{a}s^{\prime},

오토마톤은 다음 전이를 포함한다.

s\xrightarrow{\lambda(a)}s^{\prime},

여기서 $\lambda(a)\in 2^{\mathit{AP}}$ 는 $a$ 에 대응하는 원-핫 값 배정으로, 다음과 같다.

\lambda(a)=\{\pi(a)\}.

같은 내용을 불리언 형식으로 표현하면 이 레이블은 $\pi(a)$ 를 참으로, 나머지 모든 이벤트 명제와 skip을 거짓으로 지정한다.

상태 $s\in S$ 가 종료 상태이면, 즉 다음 조건을 만족하면,

\forall a\in\Sigma_{P}.\ \nexists s^{\prime}\in S\text{ such that }s\xrightarrow{a}s^{\prime},

아래와 같은 종료 후 접미부를 추가한다.

s\xrightarrow{\{\texttt{skip}\}}s.

이렇게 하면 모든 극대 유한 실행이 무한 단어가 되어 표준 LTL 의미론을 사용할 수 있다.

Varanus가 HOA 형식의 오토마톤을 생성하지만 예측 모니터는 이를 전이 시스템으로 사용한다. $\delta$ 가 유도하는 모든 무한 실행을 현재 접두부 뒤에 허용되는 연속 실행으로 취급한다. 따라서 유한 이력 $\sigma$ 를 관찰한 뒤 예측 모니터가 고려하는 연속 실행은, $\mathcal{B}_{P}$ 가 $\sigma$ 를 읽고 도달한 상태에서 여전히 생성할 수 있는 무한 명제 단어와 정확히 일치한다.

CSP 모델에서 도출한 오토마톤 $\mathcal{B}_{P}$ 는 현재 실행 접두부와 여전히 양립하는 행동의 집합을 제공한다. 유한 이력 $\sigma$ 를 읽은 뒤 예측 모니터는 $\mathcal{B}_{P}$ 에서 $\sigma$ 이후 도달한 상태로부터 이어질 수 있는 모든 무한 실행을 고려한다. 이 실행들은 CSP 모델이 계속 허용하는 미래이며, 감시 중인 LTL 속성이 반드시 만족되는지, 반드시 위반되는지, 아직 미정인지를 판별하는 데 사용한다.

이 사상은 단순한 기술적 인코딩에 그치지 않는다. CSP 이벤트는 명제 LTL로 직접 표현할 수 있는 것보다 풍부한 구조를 가질 수 있다. 예를 들어 $\mathit{move}.i$ 는 $i\in\{0,\ldots,N\}$ 인 매개변수화 이벤트로, 로봇에게 경유지 $i$ 로 이동하라고 명령함을 뜻한다. 구체적인 이벤트 $\mathit{move}.0$ , $\mathit{move}.1$ , …, $\mathit{move}.N$ 는 CSP 수준에서 서로 다르며, 본 구성에서는 $\pi(\mathit{move}.0)=m_{0}$ , $\pi(\mathit{move}.1)=m_{1}$ 처럼 서로 다른 원자 명제로 대응시킨다. 예측 모니터는 구조화된 CSP 이벤트를 직접 추론하지 않지만 그 명제 표현은 계속 구별한다. 사상에서 사라지는 것은 이벤트 사이의 구별이 아니라 매개변수화된 CSP 이벤트라는 원래의 구조 표현이다. Varanus가 원래 이벤트 구조를 사용해 관찰 이벤트를 CSP 모델과 대조하는 동안 예측 모니터는 이에 대응하는 명제 인코딩만 사용한다.

이 사상이 중요한 이유는 두 가지다. 첫째, CSP 모델을 바꾸지 않고 성숙한 오토마톤 기반 LTL 도구를 재사용할 수 있다. 둘째, Varanus가 맡는 실행 중 이벤트의 구조적 적합성 검사와, 추상화한 명제 이력에 대해 수행하는 예측 모니터링을 명확하게 분리한다.

B. 예측 모니터 구성

LTL 수식 $\varphi$ 가 주어질 때 $\mathcal{B}_{\varphi}$ 와 $\mathcal{B}_{\neg\varphi}$ 를 각각 $\varphi$ 와 $\neg\varphi$ 에 대한 뷔히 오토마톤이라고 하자. 예측 모니터는 다음 두 동기 곱에 기반한다.

A^{+}=\mathcal{B}_{P}\times\mathcal{B}_{\varphi},\qquad A^{-}=\mathcal{B}_{P}\times\mathcal{B}_{\neg\varphi}.

유한 이력 $\sigma$ 에 대해, 사상된 이력 $\pi(\sigma)$ 를 읽은 뒤 $A^{+}$ 와 $A^{-}$ 에서 각각 도달 가능한 상태 집합을 $S^{+}_{\sigma}$ 와 $S^{-}_{\sigma}$ 라고 하자. 직관적으로 $S^{+}_{\sigma}$ 는 $\varphi$ 의 만족을 여전히 허용하는 모델 부합 미래를 나타내고, $S^{-}_{\sigma}$ 는 $\varphi$ 의 위반을 여전히 허용하는 미래를 나타낸다.

정의 3. 예측 모니터의 판정

유한 이력 $\sigma$ 에 대해 예측 모니터는 다음을 반환한다.

R_{P,\varphi}(\sigma)=\begin{cases}\top&\text{if }\mathcal{L}(A^{-},S^{-}_{\sigma})=\emptyset,\\ \bot&\text{if }\mathcal{L}(A^{+},S^{+}_{\sigma})=\emptyset,\\ ?&\text{otherwise,}\end{cases}

여기서 $\mathcal{L}(A,S)$ 는 상태 집합 $S$ 에서 초기화한 오토마톤 $A$ 가 수용하는 언어를 나타낸다.

이 판정 기준은 본 연구에만 고유한 것이 아니라 예측적 런타임 검증의 표준 오토마톤 이론적 정식화를 따른다[5]. 핵심 질문은 현재 유한 이력 이후 $\mathcal{B}_{\varphi}$ 와의 곱과 $\mathcal{B}_{\neg\varphi}$ 와의 곱에 수용 가능한 연속 실행이 여전히 존재하는가이다. 전자의 언어가 비어 있으면 위반이 불가피하고, 후자가 비어 있으면 만족이 불가피하다. 그렇지 않으면 두 결과 모두 현재 실행과 양립하여 판정은 미결정으로 남는다. 따라서 기여는 새로운 예측 판정 규칙이 아니라 표준 규칙과 CSP 행동 모델의 통합이다. 허용할 미래를 외부에서 가정하지 않고 CSP 명세에서 추출하며, Varanus가 실제 관찰된 실행에 맞춰 온라인으로 지속 검증한다.

C. 통합 의미론

전체 Predictive Varanus 처리 과정은 CSP 적합성 검사와 예측적 LTL 모니터를 순차적으로 합성한 것이다.

정의 4. Predictive Varanus

CSP 모델 $P$ 와 LTL 속성 $\varphi$ 가 주어질 때, 유한 이력 $\sigma$ 에 대한 통합 모니터는 다음 함수로 정의하며,

\mathsf{PV}_{P,\varphi}(\sigma)\in\{\mathsf{rej},\top,\bot,?\}

그 값은 아래와 같다.

\mathsf{PV}_{P,\varphi}(\sigma)=\begin{cases}\mathsf{rej}&\text{if }G_{P}(\sigma)=\mathsf{rej},\\ R_{P,\varphi}(\sigma)&\text{if }G_{P}(\sigma)=\mathsf{acc}.\end{cases}

이 구분은 의미론적으로 중요하다. $\mathsf{rej}$ 판정은 감시 중인 LTL 속성의 위반을 뜻하지 않는다. 이력이 CSP 모델이 허용하는 행동을 벗어났다는 뜻이며, 이 경우 예측의 전제가 더 이상 성립하지 않는다. 반면 $\bot$ 는 모델 적합성을 유지하는 이력에서 LTL 속성이 예측적으로 위반됨을 뜻한다. 따라서 Predictive Varanus가 미리 판단하는 것은 모델에 없는 물리적 고장이나 센서 고장이 아니라, 남은 모델 부합 미래가 강제하는 임무 중단, 방문 범위 실패, 보장된 완료 같은 결과다.

IV. 사례 연구

Predictive Varanus 평가에는 기존 Varanus 연구[7]에서 사용한 모의 핵폐기물 저장소 순찰 로버와 그 CSP 모델을 재사용한다. 로버의 임무는 여러 경유지의 방사선 수준을 검사하는 것이다. 측정값은 초록·주황·빨강으로 분류한다. 초록이면 임무를 계속하지만 주황이나 빨강이면 진입점으로 돌아가 임무를 중단해야 한다. 같은 CSP 모델과 임무를 사용함으로써 일반 런타임 적합성 검사에 비해 예측적 검증이 더하는 가치를 분리해 평가할 수 있다.

CSP 모델에서 로버는 경유지 선택, 이동, 방사선 측정값에 대한 반응을 반복한다. Varanus는 높은 방사선을 감지한 뒤 진입점 대신 다른 경유지로 이동하는 등의 잘못된 행동을 탐지할 수 있다. Predictive Varanus의 목표는 로버가 모델을 따른다는 전제 아래 일부 임무 요구사항이 불가능해지거나 불가피해지는 상황을 앞서 판단하는 것이다.

다음에 정의하는 세 속성 $\varphi_{\mathit{complete}}$ , $\varphi_{\mathit{abort}}$ , $\varphi_{\mathit{cover}}$ 를 감시한다. $mc$ 는 mission_complete, $ma$ 는 mission_abort, $r$ 와 $o$ 는 각각 radiation_level.Red와 radiation_level.Orange에 대응하는 명제이며, $m_{i}$ 는 move. $i$ 에 대응하는 명제다. 첫 번째 속성은 임무를 여전히 성공적으로 완료할 수 있는지를 묻는다.

\varphi_{\mathit{complete}}=F(\neg skip\wedge mc).

모니터가 아래와 같은 접두부를 관찰하면,

\langle\texttt{mission\_start},\texttt{inspect.2},

\texttt{radiation\_level.Red}\rangle,

mission_abort가 아직 일어나지 않았더라도 이 속성은 예측적으로 거짓이 된다. CSP 모델에 따르면 해당 상태 이후의 모든 연속 실행이 진입점으로 돌아가 임무를 중단하기 때문이다. 성공적인 임무 완료는 더 이상 모델과 양립하지 않는다.

두 번째 속성은 위험한 방사선이 결국 임무 중단을 강제해야 한다는 안전 의무를 표현한다.

\varphi_{\mathit{abort}}=G((r\vee o)\rightarrow F(\neg skip\wedge ma)).

같은 접두부에 대해 이 속성은 mission_abort를 관찰하기 전에 예측적으로 참이 된다. 모델에 부합하는 모든 미래에 이제 mission_abort 이벤트가 포함되기 때문이다.

세 번째 속성은 전체 임무 방문 범위다. 정상적인 임무가 다섯 검사 경유지를 모두 방문해야 한다면 다음과 같이 쓸 수 있다.

\varphi_{\mathit{cover}}=\bigwedge_{i=1}^{5}F(\neg skip\wedge m_{i}).

낮은 방사선, 즉 초록 측정값을 받으며 임무가 진행되는 동안 이 속성은 미결정( $?$ )이다. 모델상 이제 mission_abort로만 끝날 수 있고 아직 방문하지 않은 경유지가 있다면 예측적으로 거짓이 된다. 현재 이력 접두부는 모델에 맞지만, 로버가 모델을 따른다는 전제하에 방문 요구를 달성할 수 없음을 이미 알려준다는 점에서 유용한 예다. 사람 운영자나 재계획 과정에서 활용할 수 있는 정보다.

이 예들은 CSP와 예측적 LTL을 결합하는 이유를 보여준다. CSP 모델은 잘못된 이벤트를 인식하는 데에도, 미래 이벤트를 예측하는 데에도 사용한다. 로버가 수행할 수 있는 모든 이벤트 조합을 검사하는 대신, Predictive Varanus의 판정은 로버 설계 모델을 재사용하여 검사할 연속 실행을 제한한다.

V. 평가

이 절은 Predictive Varanus의 두 평가를 제시한다. 구현은 https://github.com/AngeloFerrando/PredictiveVaranus 에 공개되어 있다. 첫째, IV절의 로버 임무를 이용해 판정의 타당성과 실제 이득을 정량 평가한다. 둘째, 모델 크기·분기 구조·종료 깊이를 통제해 변화시키는 합성 CSP 모델로 계산 부담과 확장성을 정량적으로 스트레스 시험한다.

Varanus의 비용과 예측 모니터가 더하는 비용·이득을 구분한다. 두 도구가 푸는 모니터링 과제가 같지 않으므로 직접 비교하지 않는다. 대신 CSP 적합성 검사에 예측을 추가할 때의 비용을 측정한다. 예측의 이득은 Predictive Varanus가 확정 판정을 내리는 위치와, 예측 없이 같은 결론이 나중에 명시적으로 드러나는 위치의 차이로 계산한다.

A. 로버 평가

평가의 목표는 통합 모니터가 예상한 판정을 내리는지 확인하고, 유효하지 않은 이벤트보다 몇 이벤트 먼저 예측 모니터가 결론을 내릴 수 있는지 측정하는 것이다.

1. 정성적 평가

다음 세 종류의 이력을 고려한다.

유효하지 않은 이력

일부 이력은 CSP 모델을 위반한다. 예를 들어 위험 방사선 측정 뒤에도 임무를 계속하거나, 검사하라는 지시를 받지 않은 경유지로 이동한다. 이런 경우 Varanus는 첫 불법 이벤트에서 이력을 거부한다. 이는 예측 모니터가 기존 적합성 의미론을 바꾸지 않음을 보여준다.

모델에 맞지만 속성이 예측적으로 거짓인 이력

다른 이력은 모델에 맞지만 하나 이상의 속성을 달성할 수 없다고 예측 모니터가 결론 내릴 수 있다. 위험 방사선을 감지하면, 로버가 모델을 따른다는 전제에서 임무 완료와 전체 방문 속성은 mission_abort 이벤트 전에 예측적으로 거짓이 된다. 이는 예측적 부정 판정의 가장 명확한 사례다.

모델에 맞고 속성이 예측적으로 참인 이력

세 번째는 모델에 맞으면서 속성의 만족이 이미 불가피해진 이력이다. 여기에도 로버가 모델을 따른다는 전제가 있다. 위험 방사선이 감지되면 중단 속성은 mission_abort 이벤트 전에 예측적으로 참이 된다. 반대로 모든 경유지를 검사했다면, 로버가 mission_complete 이전에 추가 이벤트를 수행하더라도 전체 방문 속성은 예측적으로 참이 된다.

요약하면 Varanus는 첫 유효하지 않은 이벤트에서 모델에 맞지 않는 이력을 거부하고, 예측 모니터는 모델에 맞는 접두부에서 불가피한 만족이나 위반을 미리 판정한다.

2. 정량적 평가

각 속성과 이력에 대해 ① Predictive Varanus가 첫 확정 판정을 내린 이벤트 위치, ② 같은 결론이 이력에 명시적으로 나타나는 더 늦은 기준 위치, ③ 두 위치 차이인 선행 이득을 기록한다. 감시한 로버 속성은 $\varphi_{\mathit{complete}}$ , $\varphi_{\mathit{cover}}$ , $\varphi_{\mathit{abort}}$ 다. 표 1은 서로 다른 27회 실행의 결과다.

표 1. 로버 사례 평가 결과. 예측 위치는 Predictive Varanus의 첫 확정 판정 위치, 기준 위치는 같은 판정이 나중에 명시적으로 드러나는 위치다.

시나리오	속성	판정	예측 위치	기준 위치	선행 이득
정상 임무	$\varphi_{\mathit{complete}}$	참	25	25	0
정상 임무	$\varphi_{\mathit{cover}}$	참	17	25	8
빨강 위험 후 중단	$\varphi_{\mathit{complete}}$	거짓	9	11	2
빨강 위험 후 중단	$\varphi_{\mathit{abort}}$	참	10	11	1
주황 위험 후 중단	$\varphi_{\mathit{complete}}$	거짓	13	15	2
빨강 위험 후 계속(모델 위반)	$\varphi_{\mathit{complete}}$	거짓	10	10	0

표 1처럼 정상 이력의 $\varphi_{\mathit{complete}}$ 는 mission_complete에서만 완료를 확정할 수 있으므로 예측 이득이 없다. 반면 마지막 경유지를 방문하면 불가피해지는 $\varphi_{\mathit{cover}}$ 는 8개 이벤트만큼 앞서 판정한다. 위험 방사선을 감지하면 $\varphi_{\mathit{complete}}$ 와 $\varphi_{\mathit{cover}}$ 는 mission_abort보다 두 이벤트 먼저 예측적으로 거짓이 되고, $\varphi_{\mathit{abort}}$ 는 한 이벤트 먼저 예측적으로 참이 된다. 유효하지 않은 이력은 Varanus가 첫 불법 동작에서 거부하므로 이득이 0이다.

임무가 더 진행된 뒤 중단되는 다른 시나리오에서도 같은 행동을 관찰했다. 각 경우 $\varphi_{\mathit{complete}}$ 와 $\varphi_{\mathit{cover}}$ 는 중단 이벤트보다 두 이벤트 먼저 확정적으로 거짓이 되고, $\varphi_{\mathit{abort}}$ 는 한 이벤트 먼저 확정적으로 참이 된다.

27회 실행 전체의 런타임 부담은 크지 않았다. 모니터링 시간은 이벤트당 $1.84$ ms이며, Varanus가 $0.19$ ms, 예측 모니터가 $1.64$ ms를 차지했다. 속성별 평균 비용은 $\varphi_{\mathit{complete}}$ 에서 $0.32$ ms, $\varphi_{\mathit{abort}}$ 에서 $0.35$ ms, $\varphi_{\mathit{cover}}$ 에서 $4.84$ ms였다. 전체 방문 검사에 더 큰 오토마톤이 필요하다는 점과 일치한다.

B. 스트레스 시험

로버 평가를 보완하기 위해 생성한 CSP 모델과 이력을 대상으로 합성 벤치마크를 수행한다. 스트레스 시험은 두 부분이다. 첫째는 조밀하게 연결된 CSP 모델의 크기를 바꾸어 상태·전이 수 증가에 따른 실행 비용을 측정한다. 둘째는 분기하는 결정 접두부 뒤에 강제되는 꼬리 구간이 이어지는 이력을 이용한다. 최종 결과가 조절 가능한 지연 뒤에 명시적으로 나타날 때 예측의 이득을 측정하기 위한 구성이다.

1. 실험 설정

실험은 Ubuntu 24.04.4 LTS, Linux 6.8.0-106-generic 환경에서 수행했다. 서버는 11세대 Intel Core i9-11900KF CPU(3.50GHz, 8코어, 16스레드)와 32GiB RAM을 갖췄다. Docker에서 CPU·메모리 제한 없이 벤치마크를 실행했다. 예측 모니터는 Python 3.8.10과 Spot 2.12를 사용하며, 기존 Varanus 백엔드는 Python 2.7.18을 사용한다.

첫 합성 벤치마크에서는 조밀하게 연결된 CSP 모델 크기를 변화시킨다. $N$ 은 생성한 모델의 상태 수이고 $L$ 은 실행 중 처리하는 이력 길이다. 두 번째 벤치마크에서는 분기하는 결정 접두부 뒤에 강제된 꼬리 구간이 이어진다. $B$ 는 결정 접두부의 분기 수, $D$ 는 깊이, $T$ 는 종료 이벤트 이전의 강제 꼬리 길이다.

2. 비용 지표

조밀한 합성 벤치마크의 각 실행에서는 한 번만 드는 전처리 비용과 이벤트당 평균 모니터링 비용을 기록한다. 전처리에는 관찰 가능한 CSP 이벤트에서 명제 집합 구성, 모델 오토마톤의 HOA 출력, 같은 명제 집합 위로 감시할 LTL 수식 변환, 예측 모니터 초기화가 포함된다. 이벤트당 비용은 Varanus 적합성 검사 비용과 예측 모니터의 추가 비용으로 나눈다. 표 2에서 $N$ 은 생성한 CSP 모델 상태 수, 이력 길이는 처리한 런타임 이벤트 수다. 전처리 시간은 일회 비용이며 나머지 열은 CSP 검증·예측 모니터링·합계의 이벤트당 평균 비용이다.

표 2. 조밀한 합성 모델의 스트레스 시험 비용. 단위는 밀리초(ms)다. 전처리는 일회 비용이고 나머지 열은 온라인 모니터링의 이벤트당 평균 비용이다.

모델 매개변수	이력 길이	전처리 시간	이벤트당 CSP 비용	이벤트당 예측 비용	이벤트당 총비용
$N=10$	$100$	95.37	0.129	0.198	0.327
$N=10$	$1000$	94.48	0.109	0.179	0.288
$N=10$	$10000$	95.31	0.100	0.176	0.276
$N=50$	$100$	1787.79	0.356	7.544	7.900
$N=50$	$1000$	1807.28	0.314	7.596	7.911
$N=50$	$10000$	1785.69	0.329	7.604	7.934
$N=100$	$100$	25207.81	0.577	64.462	65.039
$N=100$	$1000$	25120.47	0.582	65.102	65.685
$N=100$	$10000$	25106.34	0.598	65.482	66.082
$N=200$	$100$	389574.41	0.972	756.577	757.550
$N=200$	$1000$	391505.33	0.984	705.667	706.653
$N=200$	$10000$	396888.37	0.992	701.640	702.633

비용은 뚜렷한 증가 양상을 보였다. CSP 적합성 검사 자체는 $N=200$ 에서도 이벤트당 $1$ ms 미만으로 비교적 저렴했다. 반면 예측 모니터는 모델이 커질수록 온라인 비용을 지배한다. $N=10$ 에서 약 $0.2$ ms였던 이벤트당 시간이 $N=50$ 에서 약 $7.6$ ms, $N=100$ 에서 $65$ ms, $N=200$ 에서 $702$ – $757$ ms로 증가했다. $N$ 이 고정되면 이력 길이가 달라져도 이벤트당 비용은 비교적 일정하다. 온라인 비용이 전체 이력 길이보다 오토마톤 크기에 주로 좌우됨을 나타낸다.

일회 전처리 비용에서는 같은 경향이 더 강하게 나타났다. $N=10$ 에서 약 $95$ ms였던 시간이 $N=50$ 에서 약 $1.8$ 초, $N=100$ 에서 약 $25$ 초, $N=200$ 에서 약 $390$ – $397$ 초로 증가했다. 따라서 현재 구현의 주된 확장성 병목은 Varanus를 사용하는 RV 단계가 아니라, PRV 단계의 예측 모니터에 필요한 오토마톤 구성·유지 과정이다.

3. 예측 지표

두 번째 합성 벤치마크의 핵심 지표는 선행 이득이다. 생성 이력은 네 부분으로 구성된다. 여러 분기 중 하나를 따르는 초기 결정 접두부, 최종 결과가 고정되는 하나의 확정 이벤트, 그 결정이 정한 이벤트 열인 강제 꼬리, 결과를 명시하는 최종 종료 이벤트다. 확정 이벤트 이후에는 모델에 부합하는 모든 남은 실행의 판정이 같으므로 예측 모니터는 그 지점에서 결론을 내릴 것으로 기대된다. 기준 위치는 예측 없이 같은 결과가 드러나는 최종 종료 이벤트다. 벤치마크는 분기 수 $3$ 가지 $\times 2$ 가지 깊이 $\times 4$ 가지 꼬리 길이 $\times 2$ 가지 속성 $\times 2$ 가지 이력 종류로 총 96개 집계 구성을 만든다. 결과는 매우 규칙적이다. 분기 수·속성의 긍정 또는 부정·이력 종류는 측정한 이득에 영향을 주지 않고, 결정 깊이는 예측 지연과 기준 지연을 같은 상수만큼 옮긴다. 따라서 표 3에는 대표 행만 제시한다.

표 3. 결정–꼬리 벤치마크의 대표 예측 이득. 원문은 96개 전체 행 대신 대표 결과를 제시한다. 깊이

D

가 고정되면 예측 지연은 일정하고, 기준 지연은 꼬리 길이

T

에 따라 증가하며, 이득은

T

에만 좌우된다.

모델 매개변수	속성	이력 종류	예측 지연	기준 지연	선행 이득
$B=2,D=4,T=1$	succ	성공	6	8	2
$B=2,D=4,T=5$	succ	성공	6	12	6
$B=2,D=4,T=10$	succ	성공	6	17	11
$B=2,D=4,T=20$	succ	성공	6	27	21
$B=2,D=6,T=1$	succ	성공	8	10	2
$B=2,D=6,T=5$	succ	성공	8	14	6
$B=2,D=6,T=10$	succ	성공	8	19	11
$B=2,D=6,T=20$	succ	성공	8	29	21

모든 구성에서 Predictive Varanus는 결과를 명시하는 최종 이벤트보다 먼저 확정 판정을 내렸다. 선행 이득은 꼬리 길이 $T$ 에 비례해 증가했다. $T=1$ 이면 2개 이벤트, $T=5$ 이면 6개, $T=10$ 이면 11개, $T=20$ 이면 21개였다. 실행이 확정 이벤트에 도달한 뒤에는 최종 mission_complete 또는 mission_abort까지 강제되는 미래 행동이 많이 남을수록 예측의 실제 이득이 커짐을 보여준다.

4. 논의

로버 사례와 합성 스트레스 시험은 비용과 이득을 함께 보여준다. 로버 실험에서는 운영에 도움이 될 만큼 일찍 예측 판정을 얻었다. 정상 임무의 전체 방문 속성은 임무 완료보다 8개 이벤트 먼저 결론 내렸다. 위험 방사선 감지 뒤 완료·전체 방문 속성의 실패는 중단보다 두 이벤트 먼저, 중단 속성의 만족은 한 이벤트 먼저 판정했다. 이 이득은 CSP 모델에 여전히 맞는 이력에서 나타나며 예측 모니터링이 겨냥하는 상황이다. 비용 측면에서 조밀한 합성 벤치마크는 현재 시제품의 주된 확장성 병목이 예측 구성요소임을 보여준다. Varanus는 저렴하지만 큰 모델에서 예측적 LTL 모니터의 전처리와 이벤트별 검사는 비싸진다. 이는 처리 과정 자체보다 현재 구현의 한계다. 예측 모니터는 모듈이므로 CSP 적합성 계층을 바꾸지 않고 더 빠른 오토마톤 백엔드, 기호적 표현 또는 다른 예측 논리로 교체할 수 있다. 그 비용의 이득은 결정–꼬리 벤치마크에서 확인된다. 확정 지점에서 남은 행동이 정해지면 즉시 확정 판정을 반환하며, 강제 꼬리가 길어질수록 더 많이 앞서 판정한다.

종합하면 Predictive Varanus는 Varanus의 적합성 보증을 유지하면서 유용한 예측 판정을 더한다. 큰 모델에서는 부담이 커지지만, 더 긴 강제 연속 실행에서는 확정 결론을 더 일찍 얻는 대가 관계가 있다.

VI. 관련 연구

본 연구는 예측적 런타임 검증과 CSP 기반 런타임 모니터링의 접점에 있다. 모델 기반 PRV는 이미 전이 시스템·오토마톤·정적 모델이 허용하는 미래로 예측을 제한한다[5,6]. Predictive Varanus의 차이는 같은 구조화된 CSP 모델을 Varanus[7]처럼 온라인 적합성 오라클로 쓰는 동시에, 예측적 LTL 모니터링에서 허용할 미래의 근원으로 재사용한다는 점이다.

전통적 RV는 유한 접두부를 감시한다. Giannakopoulou와 Havelund는 시간적 속성을 오토마톤 기반 관찰자로 컴파일했고[1], Bauer 등은 유한 접두부에 대한 LTL·TLTL 모니터링의 표준 설명을 제시했다[2]. 예측적 RV는 모델에 부합하는 미래로 관심을 제한한다. Zhang 등은 예측적 LTL 의미론을 도입했고[5], Pinisetty 등은 시간 제약 속성으로 확장했다[6]. 이 연구들은 본 접근의 의미론적 기반이지만 CSP로 미래를 정의하지는 않는다.

프로세스 대수 측면에서 CSP는 순서·통신·동기화를 모델링하는 데 오랫동안 사용됐다. FDR[9], PAT[13], RoboChart[10]는 CSP 계열 모델의 설계 단계 가치를 보여주지만 주로 오프라인 도구다. 가장 가까운 런타임 연구는 CSP 명세를 실행 중 오라클로 재사용하는 Varanus[7]다. 그러나 여전히 적합성 모니터이므로 유효하지 않은 이벤트는 감지하지만 미래 실행을 예측적으로 추론하지 않는다. 본 연구는 이 모델 재사용 관점에 예측적 시간 추론을 더한다.

관련 로봇 연구들은 여러 관점에서 RV와 보증을 다뤘다. ROSRV와 ROSMonitoring은 ROS용 온라인 모니터링 체계를 제공하고[14,15], Desai 등의 연구와 SOTER는 런타임 추론과 안전 보증을 결합한다[16,17]. 이러한 접근이 모니터링 기반 구조나 안전 제어에 초점을 맞추는 것과 달리, 본 연구는 신뢰하는 행동 모델에 계속 맞는 실행의 예측적 진단에 집중한다.

마지막 비교 대상은 로봇의 시간 논리 기반 계획과 합성이다. Kress-Gazit 등과 Alonso-Mora 등은 시간 논리로 설계상 올바른 로봇 행동을 구성했다[18,19]. 본 기여는 이에 보완적이다. 제어기를 합성하는 대신 실행 중인 시스템을 감시하고, CSP 모델이 허용하는 행동 아래 미래 결과를 예측한다.

연구진이 아는 범위에서는 본 방식처럼 CSP 기반 런타임 적합성 모니터링과 예측적 LTL RV를 결합한 다른 접근은 없다. Predictive Varanus는 같은 CSP 모델을 관찰 이벤트 이력의 적합성 관문과 예측 모니터가 허용할 미래의 근원으로 모두 사용한다. 모델 부적합과 시간적 속성 실패의 구별을 유지하면서 더 이른 판정을 가능하게 한다.

VII. 결론

본 논문은 CSP 적합성 검사와 예측적 LTL 모니터링을 결합한 RV 처리 과정인 Predictive Varanus를 제시했다. 단일 CSP 모델을 관찰 이벤트 이력의 검증과 예측 모니터가 탐색할 미래 생성에 재사용한다. 이를 통해 무효 행동은 즉시 거부하고 유효한 접두부는 LTL 속성의 만족·위반·미결정으로 분류한다. 평가는 설계의 이득과 비용을 함께 보여준다. 로버 사례에서는 종료 이벤트보다 앞서 임무 완료·전체 방문·중단을 인식하거나 예측하여 운영에 유용한 판정을 일찍 제공했다. 합성 벤치마크에서는 CSP 검증이 가벼운 반면, 모델이 커질수록 예측 모니터가 부담의 대부분을 차지했다. 그럼에도 결정–꼬리 실험은 확정 지점 뒤 강제되는 미래 행동이 늘수록 선행 이득이 커짐을 보여준다. 종합적으로 Predictive Varanus는 Varanus의 CSP 기반 보증을 보존하고, 전체 모니터링 과정에서 단일 설계 모델을 재사용하며, 현실적인 로봇 이력에 유용한 예측 판정을 추가한다.

향후 연구는 예측 효율 개선, 부정 판정에 따른 완화 또는 행동 강제, 5값 의미론 같은 더 풍부한 판정 체계 탐색, 여러 구성요소나 여러 모델을 가진 로봇 시스템으로의 확장을 포함한다.

참고문헌

[1] D. Giannakopoulou and K. Havelund, “Automata-based verification of temporal properties on running programs,” in 16th IEEE International Conference on Automated Software Engineering (ASE 2001), 26-29 November 2001, Coronado Island, San Diego, CA, USA. IEEE Computer Society, 2001, pp. 412–416. [Online]. Available: https://doi.org/10.1109/ASE.2001.989841
[2] A. Bauer, M. Leucker, and C. Schallhart, “Runtime verification for LTL and TLTL,” ACM Trans. Softw. Eng. Methodol., vol. 20, no. 4, pp. 14:1–14:64, 2011. [Online]. Available: https://doi.org/10.1145/2000799.2000800
[3] M. Luckcuck, M. Farrell, L. A. Dennis, C. Dixon, and M. Fisher, “Formal specification and verification of autonomous robotic systems: A survey,” ACM Comput. Surv., vol. 52, no. 5, pp. 100:1–100:41, 2019. [Online]. Available: https://doi.org/10.1145/3342355
[4] M. Leucker, “Sliding between model checking and runtime verification,” in Runtime Verification, Third International Conference, RV 2012, Istanbul, Turkey, September 25-28, 2012, Revised Selected Papers, ser. Lecture Notes in Computer Science, S. Qadeer and S. Tasiran, Eds., vol. 7687. Springer, 2012, pp. 82–87. [Online]. Available: https://doi.org/10.1007/978-3-642-35632-2_10
[5] X. Zhang, M. Leucker, and W. Dong, “Runtime verification with predictive semantics,” in NASA Formal Methods - 4th International Symposium, NFM 2012, Norfolk, VA, USA, April 3-5, 2012. Proceedings, ser. Lecture Notes in Computer Science, A. Goodloe and S. Person, Eds., vol. 7226. Springer, 2012, pp. 418–432. [Online]. Available: https://doi.org/10.1007/978-3-642-28891-3_37
[6] S. Pinisetty, T. Jéron, S. Tripakis, Y. Falcone, H. Marchand, and V. Preoteasa, “Predictive runtime verification of timed properties,” Journal of Systems and Software, vol. 132, pp. 353–365, 2017. [Online]. Available: https://doi.org/10.1016/j.jss.2017.06.060
[7] M. Luckcuck, A. Ferrando, and F. Faruq, “Varanus: Runtime verification for CSP,” in Towards Autonomous Robotic Systems - 26th Annual Conference, TAROS 2025, York, UK, August 20-22, 2025, Proceedings, ser. Lecture Notes in Computer Science, A. Cavalcanti, S. Foster, and R. Richardson, Eds. Springer, 2025, pp. 259–272. [Online]. Available: https://doi.org/10.1007/978-3-032-01486-3_21
[8] A. W. Roscoe, Understanding Concurrent Systems, ser. Texts in Computer Science. Springer, 2010. [Online]. Available: https://doi.org/10.1007/978-1-84882-258-0
[9] T. Gibson-Robinson, P. J. Armstrong, A. Boulgakov, and A. W. Roscoe, “FDR3 - A modern refinement checker for CSP,” in Tools and Algorithms for the Construction and Analysis of Systems - 20th International Conference, TACAS 2014, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2014, Grenoble, France, April 5-13, 2014. Proceedings, ser. Lecture Notes in Computer Science, E. Ábrahám and K. Havelund, Eds. Springer, 2014, pp. 187–201. [Online]. Available: https://doi.org/10.1007/978-3-642-54862-8_13
[10] A. Miyazawa, P. Ribeiro, W. Li, A. Cavalcanti, J. Timmis, and J. Woodcock, “Robochart: modelling and verification of the functional behaviour of robotic applications,” Softw. Syst. Model., vol. 18, no. 5, pp. 3097–3149, 2019. [Online]. Available: https://doi.org/10.1007/s10270-018-00710-z
[11] A. Ferrando, R. C. Cardoso, M. Farrell, M. Luckcuck, F. Papacchini, M. Fisher, and V. Mascardi, “Bridging the gap between single- and multi-model predictive runtime verification,” Formal Methods Syst. Des., vol. 59, no. 1, pp. 44–76, 2021. [Online]. Available: https://doi.org/10.1007/s10703-022-00395-7
[12] A. Cavalcanti, W. Huang, J. Peleska, and J. Woodcock, “CSP and kripke structures,” in Theoretical Aspects of Computing - ICTAC 2015 - 12th International Colloquium Cali, Colombia, October 29-31, 2015, Proceedings, ser. Lecture Notes in Computer Science, M. Leucker, C. Rueda, and F. D. Valencia, Eds. Springer, 2015, pp. 505–523. [Online]. Available: https://doi.org/10.1007/978-3-319-25150-9_29
[13] J. Sun, Y. Liu, and J. S. Dong, “Model checking CSP revisited: Introducing a process analysis toolkit,” in Leveraging Applications of Formal Methods, Verification and Validation, Third International Symposium, ISoLA 2008, Porto Sani, Greece, October 13-15, 2008. Proceedings, ser. Communications in Computer and Information Science, T. Margaria and B. Steffen, Eds. Springer, 2008, pp. 307–322. [Online]. Available: https://doi.org/10.1007/978-3-540-88479-8_22
[14] J. Huang, C. Erdogan, Y. Zhang, B. M. Moore, Q. Luo, A. Sundaresan, and G. Rosu, “ROSRV: runtime verification for robots,” in Runtime Verification - 5th International Conference, RV 2014, Toronto, ON, Canada, September 22-25, 2014. Proceedings, ser. Lecture Notes in Computer Science, B. Bonakdarpour and S. A. Smolka, Eds. Springer, 2014, pp. 247–254. [Online]. Available: https://doi.org/10.1007/978-3-319-11164-3_20
[15] A. Ferrando, R. C. Cardoso, M. Fisher, D. Ancona, L. Franceschini, and V. Mascardi, “Rosmonitoring: A runtime verification framework for ROS,” in Towards Autonomous Robotic Systems - 21st Annual Conference, TAROS 2020, Nottingham, UK, September 16, 2020, Proceedings, ser. Lecture Notes in Computer Science, A. Mohammad, X. Dong, and M. Russo, Eds. Springer, 2020, pp. 387–399. [Online]. Available: https://doi.org/10.1007/978-3-030-63486-5_40
[16] A. Desai, T. Dreossi, and S. A. Seshia, “Combining model checking and runtime verification for safe robotics,” in Runtime Verification - 17th International Conference, RV 2017, Seattle, WA, USA, September 13-16, 2017, Proceedings, ser. Lecture Notes in Computer Science, S. K. Lahiri and G. Reger, Eds. Springer, 2017, pp. 172–189. [Online]. Available: https://doi.org/10.1007/978-3-319-67531-2_11
[17] A. Desai, S. Ghosh, S. A. Seshia, N. Shankar, and A. Tiwari, “SOTER: A runtime assurance framework for programming safe robotics systems,” in 49th Annual IEEE/IFIP International Conference on Dependable Systems and Networks, DSN 2019, Portland, OR, USA, June 24-27, 2019. IEEE, 2019, pp. 138–150. [Online]. Available: https://doi.org/10.1109/DSN.2019.00027
[18] H. Kress-Gazit, G. E. Fainekos, and G. J. Pappas, “Temporal-logic-based reactive mission and motion planning,” IEEE Trans. Robotics, vol. 25, no. 6, pp. 1370–1381, 2009. [Online]. Available: https://doi.org/10.1109/TRO.2009.2030225
[19] J. Alonso-Mora, J. A. DeCastro, V. Raman, D. Rus, and H. Kress-Gazit, “Reactive mission and motion planning with deadlock resolution avoiding dynamic obstacles,” Auton. Robots, vol. 42, no. 4, pp. 801–824, 2018. [Online]. Available: https://doi.org/10.1007/s10514-017-9665-6