일시적 행동 논리

이 글에는 참고문헌, 관련 독서 또는 외부 링크 목록이 수록되어 있으나 인라인 인용구가 부족하여 출처가 불분명하다. 좀 더 정밀한 인용구를 도입하여 이 기사를 개선할 수 있도록 도와주십시오.(2011년 1월) (이 템플릿 메시지를 제거하는 방법과 시기 알아보기)

시간적 행동 논리(TLA)는 시간적 논리와 행동의 논리를 결합한 레슬리 램포트가 개발한 논리다.그것은 동시 시스템의 행동을 묘사하기 위해 사용된다.

세부 사항

시간적 작용 논리에서의 문장은${\displaystyle }$[${\displaystyle A_{}}$ ${\displaystyle {}_{}}$ t ${\$ 형식이다$.$ 여기서 A는 작용이고 t는 A에 나타나는 변수의 하위 집합을 포함한다.동작은 $x{\displaystyle }$+ ${\displaystyle {}^{}}$ ${\displaystyle {\prime }^{}}$ ${\displaystyle \ast }$ ${\displaystyle y}$= ${\displaystyle {}^{}}$ {\$displaystyle x+x'*y=y'}$과 같이 프라이밍 및 비 프라이밍 변수를 포함하는 식이다$.$비주요 변수의 의미는 이 상태에서 변수의 값이다.프라이밍된 변수의 의미는 다음 상태에 있는 변수의 값이다.위의 표현식은 x의 오늘 값을 의미하며 x의 값은 x의 내일의 값과 y의 오늘의 값을 곱한 값과 같음을 의미한다.

$[{\displaystyle }$ ${\displaystyle A}$ ${\displaystyle {}_{}}$ ${\displaystyle t_{}}$ ${\$의 의미는 A가 지금 유효하거나 t에 나타나는 변수가 변하지 않는다는 것이다$$.이것은 프로그램 변수들 중 어떤 것도 값을 바꾸지 않는 더듬는 단계를 허용한다.

참고 항목

• 동적 논리(모달 논리)
• 시간 논리학
• 플러스칼
• TLA+

참조

• Lamport, Leslie (2002). Specifying Systems: The TLA⁺ Language and Tools for Hardware and Software Engineers. Addison-Wesley. ISBN 0-321-14306-X. Retrieved 2007-02-02.
• Leslie Lamport (16 December 1994), Introduction to TLA (PDF), retrieved 2010-09-17

외부 링크

• 공식 웹사이트
• "TLA+ Proof System". INRIA.
• Lamport, Leslie (2014). "Thinking for Programmers". A gentle intro to TLA+ at Build