논리식에서 기계적 표현으로
LTL 공식은 시간에 따른 행동의 조건을 표현한다. Owl은 이런 공식을 여러 종류의 오토마타로 바꾸는 명령을 제공한다. 비결정적 Büchi 오토마타와 결정적 Rabin 또는 패리티 오토마타 등은 구조와 수용 조건이 다르다.
목적에 맞는 변환 선택
뒤에서 사용할 분석 알고리즘이 요구하는 오토마타 종류에 따라 변환 경로를 고른다. 오토마타를 패리티 형식으로 바꾸거나 비결정적 표현을 결정화하는 기능도 있다. 명령 이름뿐 아니라 선택한 구성 알고리즘과 옵션을 함께 확인한다.
구성과 결과 기록
Owl은 구현된 알고리즘의 참고 정보를 명령 도움말과 서지 기능으로 확인하도록 제공한다. 재현 가능한 실험에서는 입력 공식, 도구 버전, 하위 명령과 옵션을 묶어 기록한다. 상태 수가 줄어들었는지와 의미가 보존되는지는 구분되는 평가 항목이다.
관련 문서
Spot 오토마타 도구 / Spin 모델 검사기 / NuSMV / NuXmv