확률 모델의 의미
이산 시간과 연속 시간 모델뿐 아니라 마르코프 자동자와 매개변수 모델 및 부분 관찰 모델을 다룬다. 모델 종류마다 시간과 행동 선택 및 정보의 의미가 다르므로 목적에 맞게 선택한다. 실제로 알 수 없는 상태를 완전히 관찰한다고 가정하면 원래 문제보다 쉬운 분석이 될 수 있다.
여러 입력과 정량 요구
PRISM과 JANI 같은 모델 언어 및 명시적 형식 등을 받을 수 있다. 도달 확률과 조건부 확률, 누적 보상과 장기 평균 보상 및 다목적 분석 같은 질의를 지원한다. 입력 형식의 지원과 특정 기능의 지원은 구분해 확인한다. 목표 상태와 시간 범위 및 보상 단위를 명확히 두어야 결과를 비교할 수 있다.
구성과 재현성
모듈식 solver 인터페이스로 풀이 구성을 연결하고 Python에서도 핵심 기능에 접근할 수 있다. 선택한 엔진과 수치 처리 방식이 수행 비용과 결과 해석에 영향을 준다. 분석이 끝나지 않은 결과를 요구가 만족된 것으로 처리하지 않는다. 모델과 속성 및 도구 버전을 함께 보존하고 실제 시스템이 모델의 확률 및 환경 가정을 따르는지도 검토한다.
관련 문서
PRISM 확률 모델 검사기 / Uppaal / NuXmv / What4