계산 트리 논리

이 글은 일반적인 참고문헌 목록을 포함하고 있지만, 그에 상응하는 인라인 인용구가 충분하지 않다. 보다 정확한 인용구를 도입하여 이 기사를 개선할 수 있도록 도와주십시오. (2015년 10월) (이 템플릿 메시지를 제거하는 방법 및 시기 알아보기)

계산 트리 논리(CTL)는 분기 시간 논리로서, 그 시간의 모델은 미래가 결정되지 않은 나무와 같은 구조라는 것을 의미한다. 미래에는 다른 경로가 있는데, 그 중 어느 것이든 실현되는 실제 경로가 될 수 있다.소프트웨어 또는 하드웨어 아티팩트의 공식 검증에 사용되며, 일반적으로 모델 체커로 알려진 소프트웨어 응용 프로그램에 의해, 주어진 아티팩트가 안전성 또는 강도 속성을 가지고 있는지 여부를 결정한다.예를 들어, CTL은 일부 초기 조건이 충족될 때(예: 모든 프로그램 변수가 양수 또는 2차로를 가로지르는 고속도로에서 차량이 없음) 프로그램의 모든 가능한 실행은 바람직하지 않은 조건(예를 들어, 고속도로에서 충돌하는 차량 0 또는 2대로 나누기)을 회피하도록 지정할 수 있다.이 예에서 안전 속성은 초기 조건을 만족하는 프로그램 상태에서 가능한 모든 전환을 탐구하고 그러한 모든 실행이 속성을 만족하는지 확인하는 모델 검사기로 검증될 수 있다.계산 트리 논리는 선형 시간 논리(LTL)를 포함하는 시간 로직의 클래스에 속한다.CTL에서만 표현할 수 있는 속성과 LTL에서만 표현할 수 있는 속성이 있지만, 두 로직에서 모두 표현할 수 있는 속성은 CTL*로도 표현할 수 있다.

CTL은 에드먼드 M. 클라크와 E에 의해 처음 제안되었다. 1981년 앨런 에머슨은 이를 사용하여 소위 동기화의 골격, 즉 동시 프로그램의 추상화를 합성했다.

CTL의 구문

CTL에 대해 잘 형성된 공식의 언어는 다음과 같은 문법에 의해 생성된다.

${\displaystyle {\begin{aligned}\phi &::=\bot \mid \top \mid p\mid (\neg \phi )\mid (\phi \land \phi )\mid (\phi \lor \phi )\mid (\phi \Rightarrow \phi )\mid (\phi \Leftrightarrow \phi )\\&\mid \quad {\mbox{AX }}\phi \mid {\mbox{EX }}\phi \mid {\mbox{AF }\phi \mbox{{EF }\phi \mbox{{AG }\phi \mbox{{EG }}\phi \mbox{A}}}[\phi {\mbox{U}\mbox{{\mbox{\mbox{U}\mbox}}\mbox{{pi ]\ended}}}}}}$

여기서 $p{\displaystyle }$ ${\displaystyle p}$은(는) 일련의 원자 공식에 걸쳐 있다.예를 들어$,{\displaystyle }$ { ${\displaystyle \mathrm{\neg }}$, ${\displaystyle \wedge }$, ${\displaystyle \text{AX}}$, ${\displaystyle \text{AU}}$, ${\displaystyle \text{EU}}$ ${\displaystyle \}}$ ${\displaystyle \{\neg ,\land ,{\mbox{AX},{\$mbox{\$mbox}$ 등의 모든 커넥티브를 사용할 필요는 없다.$AU},{\mbox{$$EU}}\}$은(는) 전체 연결기 집합으로 구성되며$$, 다른 연결기 집합은 이를 사용하여 정의할 수 있다.

• ${\$$A}}$은(는) '모든 경로와 함께'(불가침)를 의미한다.
• ${\displaystyle \text{E}}$ ${\$은(는) '하나 이상의 경로(존재)'를 의미한다(가급적).

예를 들어, 다음은 잘 형성된 CTL 공식이다.

${\displaystyle {\mbox{$$EF }}({\mbox{$$EG }p\오른쪽 화살표 {\mbox{$$AF }r}$)

다음은 제대로 형성된 CTL 공식은 아니다.

${\displaystyle {\mbox}EF }}{{\big (}r{\mbox{ U }}q{\big )}}}}}$

이 문자열의 문제는 $U{\displaystyle }$ ${\displaystyle U}$이(가) $A{\displaystyle }$ ${\displaystyle A}$ 또는$$ $E{\displaystyle }$ ${\displaystyle E}$과(와) 쌍을 이룰 때만 발생할 수 있다는$$ 점이다$.$

CTL은 시스템의 상태에 대한 진술을 하기 위해 원자 제안을 그것의 구성 요소로 사용한다.그런 다음 이러한 명제는 논리 연산자와 시간 연산자를 사용하여 공식으로 결합된다.

연산자

논리 연산자

논리 연산자는 보통 ones, ∨, ∧, ⇒, ⇔.이러한 연산자와 함께 CTL 공식도 참 및 거짓 부울 상수를 사용할 수 있다.

시간 연산자

시간 연산자는 다음과 같다.

• 경로에 대한 정량자
  • A φ – All: φ은 현재 상태에서 시작하는 모든 경로를 유지하여야 한다.
  • E φ – 존재함: holds이 유지되는 현재 상태에서 시작하는 경로가 하나 이상 있음.
• 경로별 정량자
  • X φ – Next: φ은 다음 상태를 유지해야 한다(이 연산자는 X 대신 N으로 표시되기도 한다).
  • G φ – Global: φ은 이후의 모든 경로를 고수해야 한다.
  • F φ – 마지막으로: eventually은 결국 (뒤의 어느 경로에서) 버텨야 한다.
  • φ U ψ – φ은 적어도 어떤 위치에서 ψ이 버틸 때까지 버텨야 한다.향후 ψ이 검증될 것임을 시사한 것이다.
  • φ W ψ – 약자: ψ은 ψ이 버틸 때까지 버텨야 한다.U와의 차이점은 ψ이 영원히 검증될 것이라는 보장이 없다는 점이다.W 연산자를 "만약에"라고 부르기도 한다.

CTL*에서는 시간 연산자를 자유롭게 혼합할 수 있다.CTL에서 운영자는 항상 하나의 경로 운영자에 이어 상태 운영자로 분류되어야 한다.아래 예제를 참조하십시오.CTL*은 CTL보다 확실히 더 표현력이 뛰어나다.

최소 연산자 집합

CTL에는 최소한의 연산자 집합이 있다.모든 CTL 공식은 이러한 연산자만 사용하도록 변환할 수 있다.이것은 모델 확인에 유용하다.최소한의 연산자 집합은 다음과 같다: {true, ∨, ¬, EG, EU, EX}.

시간 연산자에 사용되는 변환의 일부는 다음과 같다.

• EFφ == E[trueU(properties)] (Fφ == [trueU(properties)] 때문에 )
• AXφ == ¬EX(¬φ)
• AGφ == ¬EF(¬) == = E[trueU(()]
• AFφ == A[trueUφ] == ¬EG(¬φ)
• A[φUψ] == ¬(E[(¬ψ))U¬(φ∨)] ∨ EG(¬¬) )

CTL의 의미론

정의

CTL 공식은 전이 시스템을 통해 해석된다.A transition system is a triple ${\displaystyle {\mathcal {M}}=(S,{\rightarrow },L)}$, where ${\displaystyle S}$ is a set of states, ${\displaystyle {\rightarrow }\subseteq S\times S}$ is a transition relation, assumed to be serial, i.e. every state has at least one successor, and ${\$$displaystyle L}$은 주(州)에 제안 문자를 할당하는 레이블 지정 기능이다.$Let{\displaystyle \mathcal{}}$ M${\displaystyle }$=${\displaystyle }$( ${\displaystyle S}$,${\displaystyle }$→${\displaystyle L}$) ${\displaystyle {\mathcal{M}=(S,\오른쪽$ 화살표,$L)}$을(를) 변환 모델로 사용$$

$s{\displaystyle }$ ${\displaystyle \in }$ ${\displaystyle S}$ ,${\displaystyle \varphi }$ ${\displaystyle F}$ ${\displaystyle s\in$ S$,\phi \in$ F}과$($와$$) 함께, $여기$서$$F는 M {\$displaystyle$ {\\$mathcal {M}$의 언어에 대한 wffs 집합이다$.$

그런 다음 의미론적 관계$({\displaystyle M}$, ${\displaystyle s}$ ${\displaystyle \models }$ ${\displaystyle \varphi }$) ${\displaystyle({\mathcal{M},s\models \pi )}$를 $\varphi {\displaystyle }$ ${\displaystyle \pi }$에 반복적으로 정의한다$.$

1. ${\displaystyle {\Big({\mathcal {M},s)\models \top {\Big )}\land {\Big({\mathcal {M}s)\models \bot {\\Big )}}}}$
2. ${\displaystyle {\Big (}{\mathcal {M},s)\models p{\Big )}\좌우타로우 {\Big(}p\s in L){\Big )}}}}}$
3. ${\displaystyle {\big({\mathcal {M},s)\models \neg \phi {\Big )}\좌우 이동 {\Big({\mathcal {M},s)\models \pi {\Big )}}}}}$
4. ${\displaystyle {\Big (}({\mathcal {M}},s)\models \phi _{1}\land \phi _{2}{\Big )}\Leftrightarrow {\Big (}{\big (}({\mathcal {M}},s)\models \phi _{1}{\big )}\land {\big (}({\mathcal {M}},s)\models \phi _{2}{\big )}{\Big )}}$
5. ${\displaystyle {\Big (}({\mathcal {M}},s)\models \phi _{1}\lor \phi _{2}{\Big )}\Leftrightarrow {\Big (}{\big (}({\mathcal {M}},s)\models \phi _{1}{\big )}\lor {\big (}({\mathcal {M}},s)\models \phi _{2}{\big )}{\Big )}}$
6. ${\displaystyle {\Big (}({\mathcal {M}},s)\models \phi _{1}\Rightarrow \phi _{2}{\Big )}\Leftrightarrow {\Big (}{\big (}({\mathcal {M}},s)\not \models \phi _{1}{\big )}\lor {\big (}({\mathcal {M}},s)\models \phi _{2}{\big )}{\Big )}}$
7. ${\displaystyle {\bigg (}({\mathcal {M}},s)\models \phi _{1}\Leftrightarrow \phi _{2}{\bigg )}\Leftrightarrow {\bigg (}{\Big (}{\big (}({\mathcal {M}},s)\models \phi _{1}{\big )}\land {\big (}({\mathcal {M}},s)\models \phi _{2}{\big )}{\Big )}\lor {\Big (}\neg {\big (}({\mathcal {M}},s)\models \phi _{1}{\big )}\land \neg {\big (}({\mathcal {M}},s)\m오델 \phi _{2}{\big )}{\Big )}}{\bigg )}}}}}}}}}}}:$
8. ${\displaystyle {\Big (}({\mathcal {M}},s)\models AX\phi {\Big )}\Leftrightarrow {\Big (}\forall \langle s\rightarrow s_{1}\rangle {\big (}({\mathcal {M}},s_{1})\models \phi {\big )}{\Big )}}$
9. ${\displaystyle {\Big (}({\mathcal {M}},s)\models EX\phi {\Big )}\Leftrightarrow {\Big (}\exists \langle s\rightarrow s_{1}\rangle {\big (}({\mathcal {M}},s_{1})\models \phi {\big )}{\Big )}}$
10. ${\displaystyle {\Big (}({\mathcal {M}},s)\models AG\phi {\Big )}\Leftrightarrow {\Big (}\forall \langle s_{1}\rightarrow s_{2}\rightarrow \ldots \rangle (s=s_{1})\forall i{\big (}({\mathcal {M}},s_{i})\models \phi {\big )}{\Big )}}$
11. ${\displaystyle {\Big (}({\mathcal {M}},s)\models EG\phi {\Big )}\Leftrightarrow {\Big (}\exists \langle s_{1}\rightarrow s_{2}\rightarrow \ldots \rangle (s=s_{1})\forall i{\big (}({\mathcal {M}},s_{i})\models \phi {\big )}{\Big )}}$
12. ${\displaystyle {\Big (}({\mathcal {M}},s)\models AF\phi {\Big )}\Leftrightarrow {\Big (}\forall \langle s_{1}\rightarrow s_{2}\rightarrow \ldots \rangle (s=s_{1})\exists i{\big (}({\mathcal {M}},s_{i})\models \phi {\big )}{\Big )}}$
13. ${\displaystyle {\Big (}({\mathcal {M}},s)\models EF\phi {\Big )}\Leftrightarrow {\Big (}\exists \langle s_{1}\rightarrow s_{2}\rightarrow \ldots \rangle (s=s_{1})\exists i{\big (}({\mathcal {M}},s_{i})\models \phi {\big )}{\Big )}}$
14. ${\displaystyle {\bigg (}({\mathcal {M}},s)\models A[\phi _{1}U\phi _{2}]{\bigg )}\Leftrightarrow {\bigg (}\forall \langle s_{1}\rightarrow s_{2}\rightarrow \ldots \rangle (s=s_{1})\exists i{\Big (}{\big (}({\mathcal {M}},s_{i})\models \phi _{2}{\big )}\land {\big (}\forall (j<i)({\mathcal {M}},s_{j})\models \phi _{1}{\big )}{\Big )}{\bigg )}}$
15. ${\displaystyle {\bigg (}({\mathcal {M}},s)\models E[\phi _{1}U\phi _{2}]{\bigg )}\Leftrightarrow {\bigg (}\exists \langle s_{1}\rightarrow s_{2}\rightarrow \ldots \rangle (s=s_{1})\exists i{\Big (}{\big (}({\mathcal {M}},s_{i})\models \phi _{2}{\big )}\land {\big (}\forall (j<i)({\mathcal {M}},s_{j})\models \phi _{1}{\big )}{\Big )}{\bigg )}}$

CTL 특성화

위의 규칙 10–15는 모델에서 계산 경로를 참조하며, 궁극적으로 "계산 트리"의 특성을 나타내는 것이다; 그것들은 주어진 상태 $s{\displaystyle }$ ${\displaystyle s}$에 뿌리를 둔 무한 심층 계산 트리의 특성에 대한 주장이다$.$

의미 동등성

공식 $form{\displaystyle }$ ${\displaystyle \pi }$과(와) $\psi {\displaystyle }$ ${\displaystyle \psi }$은(는) 어떤 모델에서도 다른 모델을 만족하는 상태가 충족되면 의미론적으로 동등하다고 한다$$.$is{\displaystyle }$ ${\displaystyle \varphi }${ ${$ {\$displaystyle \pi \equiv$ \$psi }$으로 표시됨

${\displaystyle \mathrm{A}}$와 E는 각각 범용 ${\displaystyle 및}$ 실존 연산 경로 정량자로 이중임을 알 수 있다: $\neg {\displaystyle \mathrm{}}$ A ≡ ${\displaystyle \equiv }$ ${\displaystyle \mathrm{E}}$ ${\displaystyle \mathrm{\neg }}$ { { \ \ \$\displaystyle$ \$neg$A\$Phi \equiv$ E$\neg$ \$Phi$ $\}.$

게다가 G와 F도 그렇다.

따라서 De Morgan의 법칙의 예는 CTL로 공식화될 수 있다.

$\displaystyle \neg AF\phi \equiv EG\neg \phi }$

$\displaystyle \neg EF\phi \equiv AG\neg \phi }$

$\displaystyle \neg AX\phi \equiv EX\neg \phi }$

CTL 시간 연결부의 하위 집합이 $E{\displaystyle }$ ${\displaystyle U}$ ${\displaystyle EU$${\displaystyle }${${\displaystyle \mathrm{AX},}$ ${\displaystyle \mathrm{EX}\}}$ ${\displaystyle \{AX,EX\},$ {${\displaystyle E}$ G${\displaystyle }$, ${\displaystyle A}$ ${\displaystyle F}$, ${\displaystyle A}$ ${\displaystyle U}$ ${\displaystyle \}}$ ${\displaysty \{EG,$$AF$} 중 하나 이상이면$$ 적절한 ID를 사용하여 표시할 수 있다.$AU\}$과(와) 부울 커넥티브.

아래의 중요한 동등성은 확장법이라고 불린다. 그들은 CTL 결합의 검증을 그 후계자를 향해 제때에 펼치게 한다.

$\displaystyle AG\phi \equiv \phi \land AXAG\pi }$

$\displaystyle EG\phi \equiv \phi \land EXEG\pi }$

$\displaystyle AF\phi \equiv \phi \lor AXAF\phi }$

$\displaystyle EF\phi \equiv \phi \lor EXEF\pi }$

$\displaystyle A[\phi U\psi ]\equiv \psi \lor (\phi \land AXA[\phi U\psi ])}$

${\displaystyle E[\phi U\psi ]\equiv \psi \lor(\phi \land EXE[\phi U\psi ])}$

예

"P"는 "초콜릿을 좋아한다"는 뜻이고 Q는 "밖이 따뜻하다"는 뜻이다."

• AG.P

앞으로 무슨 일이 있어도 초콜릿을 좋아하겠다"고 말했다.

• 에프피

"내가 언젠가 초콜릿을 좋아하게 될지도 몰라, 적어도 하루 정도는."

• AF.EG.P.

"내가 남은 시간 동안 갑자기 초콜릿을 좋아하게 되는 것은 언제나 가능한 일이다."(참고: 내 인생은 유한한 반면, G는 무한하기 때문에, 내 남은 인생만이 아니다).

• EG.AFP

그는 "앞으로 (E) 어떤 일이 일어나느냐에 따라 남은 시간(G) 동안 내 앞에 있는 (AF)초콜릿 립싱크를 적어도 한 번은 보장받을 수 있을 것"이라고 말했다.하지만, 만약 어떤 일이 잘못되면, 모든 내기는 틀리고, 내가 초콜릿을 좋아할지 여부에 대한 보장은 없어."

다음 두 가지 예는 연산자가 경로 연산자(A 또는 E)와 함께 자격을 얻지 못할 때까지 CTL과 CTL*의 차이를 보여준다.

• AG(PUQ)

"지금부터 밖이 따뜻해질 때까지 나는 매일 초콜릿을 좋아할 거야.일단 밖이 따뜻해지면, 내가 초콜릿을 더 이상 좋아할지 여부에 대한 모든 내기가 없어진다.아, 그리고 결국 바깥은 단 하루만이라도 따뜻해질 수 있도록 보장되어 있어."

• EF(EX.P)U(AG)Q))

"그럴 수도 있다. 결국 영원히 따뜻해질 때가 올 것이다.Q) 그리고 그 시간 이전에 내가 다음날 초콜릿을 좋아하게 할 수 있는 방법이 항상 있을 것이다(EX).P)."

다른 로직과의 관계

계산 트리 논리(CTL)는 모달 μ 미적분뿐만 아니라 CTL*의 하위 집합이다.CTL은 알루르, 헨징어, 쿠퍼만의 교류 시간적 논리(ATL)의 일부분이기도 하다.

계산 트리 논리(CTL)와 선형 시간 논리(LTL)는 모두 CTL*의 하위 집합이다. CTL과 LTL은 동등하지 않고 공통 하위 집합이 있는데, 이는 CTL과 LTL의 적절한 하위 집합이다.

• FG.P는 LTL에 존재하지만 CTL에는 존재하지 않는다.
• AG(P⇒)(EX).Q)mb(EXQ)) 및 AG.EF.P는 CTL에 존재하지만 LTL에는 존재하지 않는다.

확장

CTL은 2차 정량화 $\exists {\displaystyle \mathrm{}}$ ${\displaystyle p}$ ${\displaystyle \exists$ p$}$과(${\displaystyle 와}$)$\$ p {\$displaystyle$ \$forall$ p$}$로 확장되어 정량화된 계산 트리 로직(QCTL)이$$ 있다.^[1]두 가지 의미론이 있다.

• 나무의 의미론우리는 계산 트리의 노드에 라벨을 붙인다.QCTL* = QCTL = 나무 위의 MSO.모델 점검과 만족도는 탑 완성이다.
• 구조 의미론우리는 주(州)에 라벨을 붙인다.QCTL* = QCTL = 그래프 위의 MSO모델 확인은 PSPACE-완전하지만 만족은 이해할 수 없다.

구조 의미론적 QCTL 모델 점검 문제에서 QBF 해결사 활용을 위해 TQBF(정량화된 부울 공식)로의 축소가 제안되었다.^[2]

참고 항목

• 확률론적 CTL
• 공정한 계산 트리 논리
• 선형 시간 논리학

참조

• E.M. Clarke; E.A. Emerson (1981). "Design and synthesis of synchronisation skeletons using branching time temporal logic" (PDF). Logic of Programs, Proceedings of Workshop, Lecture Notes in Computer Science. Springer, Berlin. 131: 52–71.
• Michael Huth; Mark Ryan (2004). Logic in Computer Science (Second Edition). Cambridge University Press. p. 207. ISBN 978-0-521-54310-1.
• Emerson, E. A.; Halpern, J. Y. (1985). "Decision procedures and expressiveness in the temporal logic of branching time". Journal of Computer and System Sciences. 30 (1): 1–24. doi:10.1016/0022-0000(85)90001-7.
• Clarke, E. M.; Emerson, E. A. & Sistla, A. P. (1986). "Automatic verification of finite-state concurrent systems using temporal logic specifications". ACM Transactions on Programming Languages and Systems. 8 (2): 244–263. doi:10.1145/5397.5399.
• Emerson, E. A. (1990). "Temporal and modal logic". In Jan van Leeuwen (ed.). Handbook of Theoretical Computer Science, vol. B. MIT Press. pp. 955–1072. ISBN 978-0-262-22039-2.

외부 링크

• CTL의 티칭 슬라이드