본 논문은 안전에 민감한 환경에서 에이전트의 안전 사양 만족을 보장하는 방법을 다룬다. 특히, 확률적 계산 트리 로직(PCTL)으로 표현되는 더 일반적인 시간적 속성을 지원하는 새로운 접근 방식을 제시한다. 주요 기여는 다음과 같다. 첫째, 안전한 PCTL 사양 합성을 위한 이론적 프레임워크를 개발하고 CPCTL이라는 안전한 PCTL의 부분집합을 정의한다. CPCTL의 표현력이 합성 문제에 적합함을 보여준다. 둘째, 이러한 결과를 활용하여 더 일반적인 시간적 속성에 대한 합성 문제를 해결하기 위한 새로운 가치 반복 기반 알고리즘을 제안하고, 방법의 건전성과 완전성을 증명한다.