2
기본적으로 모델 검사는 시스템이 만족해야하는 모델 'm'(시스템의 동작 설명)과 'p'속성을 처리합니다. 두 아티팩트 모두를 사용하여 모델 검사기가 모델이 특성을 충족시키는 지 여부를 판별합니다.모델을 LTL로 표현
제 질문은 LTL 수식으로 'm'모델을 지정하고 LTL 'm'으로 모델이 'p'속성을 충족시키는 지 확인할 수 있는지입니다.
이론적으로 우리는 LTL 공식 'p'에 대해 하나와 모델 'm'에 대해 설명하는 LTL 속성에 대해 두 가지 Büchi 오토 마톤을 생성 할 수 있기 때문에 이론적으로이 접근법이 효과가 있다고 생각합니다. 두 개의 비 결정적 오토마타의 교집합이 비어있는 경우 LTL로 모델 'm'이 속성을 충족시킵니다.
누군가 내게 힌트를 줄 수 있습니까? 가능한가?