확률 이산 시간 시스템의 유한 시간 안전 및 회피-도달 검증

본 논문은 확률 이산 시간 동역학 시스템의 유한 시간 안전 및 회피-도달 검증을 연구한다. 목표는 미리 정의된 유한 시간 수평선 내에서 안전 집합에서 초기 상태로 시작하는 시스템이 안전 집합을 탈출할 확률(안전 검증) 또는 처음 목표와 만날 때까지 안전 집합 내에 머물며 목표 집합에 도달할 확률(회피-도달 검증)의 하한 및 상한을 확인하는 것이다. 우리는 이러한 경계를 정의하는 새로운 장벽 같은 충분 조건을 도입하며, 이는 기존 조건을 보완하거나 간극을 메운다. 마지막으로, 우리는 두 가지 예를 통해 이러한 조건의 유효성을 입증한다.