공식적인 방법 : [] <> TLA에서 무한 자주 (항상 최후에)

Question

TLA에서의 나의 이해에서, 최종 행동 (<>)은 다음 상태에서 말더듬이가 일어나는 것을 허용하지 않습니다. 그러면 무한히 자주 ([] <>)의 경우 다음 상태 변수가 더듬는 것이 허용되지 않는다는 뜻입니까?

기상 조건의 예를 들어 보면, 무한히 자주 1 년 내에 여러 날 (우리는 언제 일어날 지 모릅니다)으로 설명 될 수 있지만 비가 내리고 비가 오는 날에는 날씨가 맑아야합니다.

내 이해는 무한히 자주 맞습니까? 내가 틀렸다면 나를 바로 잡아라.

감사합니다. 시간을 거기에 지적되지 즉

Answer 1

속성 []<> ϕ이

• 이 <>[] ¬ϕ를 확인하지 않습니다 무한한 길이와
• 을 가지고 흔적에 의해 확인되고, 그 후에 ϕ 결정적 false 영원히

입니다

[] ϕ을 만족하는 무한한 자취도 []<> ϕ 전자는 후자보다 강하기 때문에 반대는 반드시 그런 것은 아닙니다.

[]<> it_rains_today 같은 문은 다음과 같은 흔적에 의해 만족 될 것이다 :

• 추적 s.t.을 하루 종일 끊임없이 비가 내린다. 영원을 위해
• 추적 s.t. 매일 영원히 비가 내린다.
• 추적 s.t. 10 년마다 1 년 동안 비가 내린다. 영원을 위해
• 추적 s.t. 모든 영원을 위해 1 천만 년에 1 일씩 비가 내린다.

그런 사건이 어떤 종류의 규칙에도 적용될 필요는 없다는 점에 유의해야한다. 유일한 요구 사항은 이 없으므로 영원히 완전히 비가 내리는 시점이 없습니다..