2014-10-31 1 views
0

CTL로 가능하다는 것을 알고 있습니다. 그렇다고 말할 수 있습니까선형 시간 논리 질문

「어느 시점부터는 항상 p가 가능합니다」.

LTL을 사용합니다.

+0

나는 LTL이 가능성의 개념을 표현할 수 있다고 생각하지 않는다. – hcs

답변

1

FGp는 후속 세트의 전체 집합이 p 인 상태 (적어도 하나)가 있음을 의미합니다. 따라서 프로세스가 진행되는 시점이 있습니다.

여기서 Fp는 P가 마지막으로 보유 할 것임을 의미합니다 (후속 경로의 어딘가에 있음). 및 Gp는 p가 현재 노드의 모든 후속 노드에서 발생 함을 의미합니다.