모델의 확률과 선택
이산 시간과 연속 시간 마르코프 체인 및 마르코프 결정 과정 등을 지원한다. 확률적 사건과 여러 행동 중 선택이 함께 있을 때는 두 개념을 구분해 모델링해야 한다. 실제 시스템의 확률을 어떻게 얻었는지와 전이의 가정이 맞는지가 계산 결과의 의미를 결정한다.
확률과 보상의 질의
PCTL과 CSL 및 LTL 계열의 명세로 모델의 성질을 기술한다. 특정 상태에 도달할 확률이나 누적 비용 및 보상처럼 수량적인 요구도 다룬다. 질문의 시간 범위와 초기 상태를 바꾸면 같은 모델에서도 다른 답을 얻을 수 있다. 단순한 통과 표시보다 어떤 질의에 대한 결과인지 기록한다.
정확한 모델과 근사 분석
상태 공간 탐색과 수치 풀이를 바탕으로 분석하며 이산 사건 시뮬레이션을 이용한 근사 검사도 제공한다. 시뮬레이션의 추정 결과를 전체 모델에 대한 같은 보증으로 받아들이지 않는다. 모델 밖의 구현이나 확률 추정 오류까지 자동으로 해결하는 도구는 아니다. 입력 자료와 알고리즘 설정 및 수치 기준을 함께 보존한다.
관련 문서
Storm 확률 모델 검사기 / Uppaal / NuSMV / TLAplus