선형 시제 논리

논리학에서 선형 시제 논리(線型時制論理, 영어: linear temporal logic, 약자 LTL)는 선형 이산 시간에 대한 여러 가지 양상을 갖춘, 시제 논리의 하나이다. PTL(Propositional temporal logic)이라고도 한다.^[1]

통사론

선형 시제 논리의 논리식은 원자 명제의 유한 집합 ${\displaystyle \operatorname {AP} \sqcup \{\top ,\bot \}}$ 및 다음과 같은 논리 연산 기호들로부터 재귀적으로 정의된다.

• (명제 논리의 기호) ${\displaystyle \land }$, ${\displaystyle \lor }$, ${\displaystyle \lnot }$, ${\displaystyle \implies }$ 등등
• (다음, 영어: next) ${\displaystyle \bigcirc }$
• (결국, 영어: eventually) ${\displaystyle \Diamond }$
• (항상, 영어: always) ${\displaystyle \Box }$
• (언틸, 영어: until) ${\displaystyle {\mathsf {U}}}$
• (약한 언틸, 영어: weak until) ${\displaystyle {\mathsf {W}}}$
• (풀기, 영어: release) ${\displaystyle {\mathsf {R}}}$

이들 기호는 다음과 같은 우선순위를 가진다.

• (일항 연산) ${\displaystyle \lnot }$, ${\displaystyle \bigcirc }$, ${\displaystyle \Diamond }$, ${\displaystyle \Box }$
• (명제 논리 밖의 이항 연산) ${\displaystyle {\mathsf {U}}}$, ${\displaystyle {\mathsf {W}}}$, ${\displaystyle {\mathsf {R}}}$
• (명제 논리의 이항 연산) ${\displaystyle \land }$, ${\displaystyle \lor }$, ${\displaystyle \implies }$

이들 기호는 ${\displaystyle \{\operatorname {AP} ,\land ,\lnot ,\bigcirc ,{\mathsf {U}}\}}$로부터 다음과 같이 유도된다.

• ${\displaystyle P\lor Q=\lnot (\lnot P\land \lnot Q)}$
• ${\displaystyle P\implies Q=\lnot P\lor Q}$
• ${\displaystyle \top =p\implies p\qquad (p\in \operatorname {AP} )}$
• ${\displaystyle \bot =\lnot \top }$
• ${\displaystyle P\operatorname {\mathsf {W}} Q=\lnot ((P\land \lnot Q)\operatorname {\mathsf {U}} {(}\lnot P\land \lnot Q))}$
• ${\displaystyle P\operatorname {\mathsf {R}} Q=\lnot (\lnot P\operatorname {\mathsf {U}} \lnot Q)}$
• ${\displaystyle \Diamond P=\top \operatorname {\mathsf {U}} P}$
• ${\displaystyle \Box P=P\operatorname {\mathsf {W}} \bot =\bot \operatorname {\mathsf {R}} P}$

이들 기호는 다음과 같이 해석된다.

• ${\displaystyle \bigcirc P}$: 바로 다음 번에 ${\displaystyle P}$가 참이다.
• ${\displaystyle \Diamond P}$: 결국/언젠가 ${\displaystyle P}$가 참이다.
• ${\displaystyle \Box P}$: 항상/언제나 ${\displaystyle P}$가 참이다.
• ${\displaystyle \Diamond \Box P}$: 언젠가부터 영원히 ${\displaystyle P}$가 참이다.
• ${\displaystyle \Box \Diamond P}$: 무한 개의 시점에서 ${\displaystyle P}$가 참이다.
• ${\displaystyle P\operatorname {\mathsf {U}} Q}$: 언젠가 ${\displaystyle Q}$가 참이기 바로 전까지 줄곧 ${\displaystyle P}$가 참이다.
• ${\displaystyle P\operatorname {\mathsf {W}} Q}$: ${\displaystyle Q}$가 참이기 바로 전까지 줄곧 ${\displaystyle P}$가 참이다.
• ${\displaystyle P\operatorname {\mathsf {R}} Q}$: ${\displaystyle P}$가 참일 때까지 줄곧 ${\displaystyle Q}$가 참이다.

의미론

원자 명제 집합의 멱집합 위의 무한 열

${\displaystyle w=(w_{0},w_{1},w_{2},\dots )\in (2^{\operatorname {AP} })^{\omega }}$

및 선형 시제 논리식 ${\displaystyle P}$가 주어졌다고 하자. 또한,

${\displaystyle w^{j}=(w_{j},w_{j+1},w_{j+2},\dots )}$

와 같이 쓰자. 그렇다면, ${\displaystyle w}$가 ${\displaystyle P}$를 만족시킨다는 것은 ${\displaystyle w\models P}$와 같이 표기하며, 다음과 같이 재귀적으로 정의된다.

• ${\displaystyle w\models \top \iff \top }$
• ${\displaystyle w\models \bot \iff \bot }$
• ${\displaystyle w\models p\iff p\in w_{0}\qquad (p\in \operatorname {AP} )}$
• ${\displaystyle w\models P\land Q\iff w\models P\land w\models Q}$
• ${\displaystyle w\models P\lor Q\iff w\models P\lor w\models Q}$
• ${\displaystyle w\models \lnot P\iff w\not \models P}$
• ${\displaystyle w\models P\implies Q\iff w\not \models P\lor w\models Q}$
• ${\displaystyle w\models \bigcirc P\iff w^{1}\models P}$
• ${\displaystyle w\models \Diamond P\iff \exists j\in \{0,1,\dots \}\colon w^{j}\models P}$
• ${\displaystyle w\models \Box P\iff \forall j\in \{0,1,\dots \}\colon w^{j}\models P}$
• ${\displaystyle w\models \Diamond \Box P\iff \exists j\in \{0,1,\dots \}\forall k\in \{j,j+1,\dots \}\colon w^{k}\models P}$
• ${\displaystyle w\models \Box \Diamond P\iff \forall j\in \{0,1,\dots \}\exists k\in \{j,j+1,\dots \}\colon w^{k}\models P}$
• ${\displaystyle w\models P\operatorname {\mathsf {U}} Q\iff \exists j\in \{0,1,\dots \}\colon w^{0},\dots ,w^{j-1}\models P\land w^{j}\models Q}$
• ${\displaystyle w\models P\operatorname {\mathsf {W}} Q\iff \exists j\in \{0,1,\dots ,\infty \}\colon w^{0},\dots ,w^{j-1}\models P\land w^{j}\models Q}$
• ${\displaystyle w\models P\operatorname {\mathsf {R}} Q\iff \exists j\in \{0,1,\dots ,\infty \}\colon w^{0},\dots ,w^{j}\models Q\land w^{j}\models P}$

(물론, ${\displaystyle w\models p}$(${\displaystyle p\in \operatorname {AP} }$), ${\displaystyle w\models \lnot P}$, ${\displaystyle w\models P\land Q}$, ${\displaystyle w\models \bigcirc P}$, ${\displaystyle w\models P\operatorname {\mathsf {U}} Q}$의 정의로부터 나머지 정의들을 유도할 수 있다.) 이에 따라, 선형 시제 논리식 ${\displaystyle P}$는 의미론적으로 집합

${\displaystyle {\models }^{-1}(P)\subseteq (2^{\operatorname {AP} })^{\omega }}$

에 대응된다.

성질

선형 시제 논리식에 대하여, 다음과 같은 논리적 동치·함의 관계가 성립한다.

• 쌍대 법칙
  • ${\displaystyle \lnot \bigcirc P\iff \bigcirc \lnot P}$
  • ${\displaystyle \lnot \Diamond P\iff \Box \lnot P}$
  • ${\displaystyle \lnot \Box P\iff \Diamond \lnot P}$
  • ${\displaystyle \lnot (P\operatorname {\mathsf {U}} Q)\iff (P\land \lnot Q)\operatorname {\mathsf {W}} {(}\lnot P\land \lnot Q)\iff \lnot P\operatorname {\mathsf {R}} \lnot Q}$
  • ${\displaystyle \lnot (P\operatorname {\mathsf {W}} Q)\iff (P\land \lnot Q)\operatorname {\mathsf {U}} {(}\lnot P\land \lnot Q)}$
  • ${\displaystyle \lnot (P\operatorname {\mathsf {R}} Q)\iff (\lnot P\operatorname {\mathsf {U}} \lnot Q)}$
• 멱등 법칙
  • ${\displaystyle \Diamond \Diamond P\iff \Diamond P}$
  • ${\displaystyle \Box \Box P\iff \Box P}$
  • ${\displaystyle P\operatorname {\mathsf {U}} {(}P\operatorname {\mathsf {U}} Q)\iff P\operatorname {\mathsf {U}} Q\iff (P\operatorname {\mathsf {U}} Q)\operatorname {\mathsf {U}} Q}$
  • ${\displaystyle P\operatorname {\mathsf {W}} {(}P\operatorname {\mathsf {W}} Q)\iff P\operatorname {\mathsf {W}} Q\iff (P\operatorname {\mathsf {W}} Q)\operatorname {\mathsf {W}} Q}$
  • ${\displaystyle P\operatorname {\mathsf {R}} {(}P\operatorname {\mathsf {R}} Q)\iff P\operatorname {\mathsf {R}} Q\iff (P\operatorname {\mathsf {R}} Q)\operatorname {\mathsf {R}} Q}$
• 흡수 법칙
  • ${\displaystyle \Diamond \Box \Diamond P\iff \Box \Diamond P}$
  • ${\displaystyle \Box \Diamond \Box P\iff \Diamond \Box P}$
• 분배 법칙
  • ${\displaystyle \bigcirc (P\operatorname {\mathsf {U}} Q)\iff \bigcirc P\operatorname {\mathsf {U}} \bigcirc Q}$
  • ${\displaystyle \bigcirc (P\operatorname {\mathsf {W}} Q)\iff \bigcirc P\operatorname {\mathsf {W}} \bigcirc Q}$
  • ${\displaystyle \bigcirc (P\operatorname {\mathsf {R}} Q)\iff \bigcirc P\operatorname {\mathsf {R}} \bigcirc Q}$
  • ${\displaystyle \Diamond (P\lor Q)\iff \Diamond P\lor \Diamond Q}$
    • ${\displaystyle \Diamond (P\land Q)\implies \Diamond P\land \Diamond Q}$
  • ${\displaystyle \Box (P\land Q)\iff \Box P\land \Box Q}$
    • ${\displaystyle \Box (P\lor Q)\Longleftarrow \Box P\lor \Box Q}$
• 전개 법칙
  • ${\displaystyle \Diamond P\iff P\lor \bigcirc \Diamond P}$
  • ${\displaystyle \Box P\iff P\land \bigcirc \Box P}$
  • ${\displaystyle P\operatorname {\mathsf {U}} Q\iff Q\lor (P\land \bigcirc (P\operatorname {\mathsf {U}} Q))}$
  • ${\displaystyle P\operatorname {\mathsf {W}} Q\iff Q\lor (P\land \bigcirc (P\operatorname {\mathsf {W}} Q))}$
  • ${\displaystyle P\operatorname {\mathsf {R}} Q\iff P\lor (Q\land \bigcirc (P\operatorname {\mathsf {R}} Q))}$
  • ${\displaystyle (X\Longleftarrow (Q\lor (P\land \bigcirc X)))\implies (X\Longleftarrow P\operatorname {\mathsf {U}} Q)}$
  • ${\displaystyle (X\implies (Q\lor (P\land \bigcirc X)))\implies (X\implies P\operatorname {\mathsf {W}} Q)}$
• 기타 법칙
  • ${\displaystyle \Box P\implies \underbrace {\bigcirc \cdots \bigcirc } _{n}\,P\implies \Diamond P\qquad (n\in \{0,1,\dots \})}$
  • ${\displaystyle Q\operatorname {\mathsf {R}} P\lor P\operatorname {\mathsf {U}} Q\implies P\operatorname {\mathsf {W}} Q}$
  • ${\displaystyle P\operatorname {\mathsf {W}} Q\iff P\operatorname {\mathsf {U}} Q\lor \Box Q}$
  • ${\displaystyle P\operatorname {\mathsf {U}} Q\iff P\operatorname {\mathsf {W}} Q\land \Diamond Q}$
  • ${\displaystyle P\operatorname {\mathsf {W}} Q\iff (\lnot P\lor Q)\operatorname {\mathsf {R}} {(}P\lor Q)}$
  • ${\displaystyle P\operatorname {\mathsf {R}} Q\iff (\lnot P\land Q)\operatorname {\mathsf {W}} {(}P\land Q)}$