선형 시제 논리

틀:위키데이터 속성 추적 논리학에서 선형 시제 논리(線型時制論理, 틀:Llang, 약자 LTL)는 선형 이산 시간에 대한 여러 가지 양상을 갖춘, 시제 논리의 하나이다. PTL(Propositional temporal logic)이라고도 한다.

통사론

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

• (명제 논리의 기호) $\wedge$, $\vee$, $\mathrm{\neg }$, $⟹$ 등등
• (다음, 틀:Llang) $◯$
• (결국, 틀:Llang) $◊$
• (항상, 틀:Llang) $◻$
• (언틸, 틀:Llang) $𝖴$
• (약한 언틸, 틀:Llang) $𝖶$
• (풀기, 틀:Llang) $𝖱$

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

• (일항 연산) $\mathrm{\neg }$, $◯$, $◊$, $◻$
• (명제 논리 밖의 이항 연산) $𝖴$, $𝖶$, $𝖱$
• (명제 논리의 이항 연산) $\wedge$, $\vee$, $⟹$

이들 기호는 $\{\mathrm{AP},\wedge ,\mathrm{\neg },◯,𝖴\}$로부터 다음과 같이 유도된다.

• $P\vee Q=\mathrm{\neg }(\mathrm{\neg }P\wedge \mathrm{\neg }Q)$
• $P⟹Q=\mathrm{\neg }P\vee Q$
• $\mathrm{\top }=p⟹p(p\in \mathrm{AP})$
• $\mathrm{\perp }=\mathrm{\neg }\mathrm{\top }$
• $P𝖶Q=\mathrm{\neg }((P\wedge \mathrm{\neg }Q)𝖴(\mathrm{\neg }P\wedge \mathrm{\neg }Q))$
• $P𝖱Q=\mathrm{\neg }(\mathrm{\neg }P𝖴\mathrm{\neg }Q)$
• $◊P=\mathrm{\top }𝖴P$
• $◻P=P𝖶\mathrm{\perp }=\mathrm{\perp }𝖱P$

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

• $◯P$: 바로 다음 번에 $P$가 참이다.
• $◊P$: 결국/언젠가 $P$가 참이다.
• $◻P$: 항상/언제나 $P$가 참이다.
• $◊◻P$: 언젠가부터 영원히 $P$가 참이다.
• $◻◊P$: 무한 개의 시점에서 $P$가 참이다.
• $P𝖴Q$: 언젠가 $Q$가 참이기 바로 전까지 줄곧 $P$가 참이다.
• $P𝖶Q$: $Q$가 참이기 바로 전까지 줄곧 $P$가 참이다.
• $P𝖱Q$: $P$가 참일 때까지 줄곧 $Q$가 참이다.

의미론

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

$w=(w_0,w_1,w_2,\dots )\in (2^{\mathrm{AP}}{)}^{\omega }$

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

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

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

• $w\models \mathrm{\top }⟺\mathrm{\top }$
• $w\models \mathrm{\perp }⟺\mathrm{\perp }$
• $w\models p⟺p\in w_0(p\in \mathrm{AP})$
• $w\models P\wedge Q⟺w\models P\wedge w\models Q$
• $w\models P\vee Q⟺w\models P\vee w\models Q$
• $w\models \mathrm{\neg }P⟺w\models ̸P$
• $w\models P⟹Q⟺w\models ̸P\vee w\models Q$
• $w\models ◯P⟺w^1\models P$
• $w\models ◊P⟺\mathrm{\exists }j\in \{0,1,\dots \}:w^j\models P$
• $w\models ◻P⟺\mathrm{\forall }j\in \{0,1,\dots \}:w^j\models P$
• $w\models ◊◻P⟺\mathrm{\exists }j\in \{0,1,\dots \}\mathrm{\forall }k\in \{j,j+1,\dots \}:w^k\models P$
• $w\models ◻◊P⟺\mathrm{\forall }j\in \{0,1,\dots \}\mathrm{\exists }k\in \{j,j+1,\dots \}:w^k\models P$
• $w\models P𝖴Q⟺\mathrm{\exists }j\in \{0,1,\dots \}:w^0,\dots ,w^{j-1}\models P\wedge w^j\models Q$
• $w\models P𝖶Q⟺\mathrm{\exists }j\in \{0,1,\dots ,\mathrm{\infty }\}:w^0,\dots ,w^{j-1}\models P\wedge w^j\models Q$
• $w\models P𝖱Q⟺\mathrm{\exists }j\in \{0,1,\dots ,\mathrm{\infty }\}:w^0,\dots ,w^j\models Q\wedge w^j\models P$

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

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

에 대응된다.

성질

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

• 쌍대 법칙
  • $\mathrm{\neg }◯P⟺◯\mathrm{\neg }P$
  • $\mathrm{\neg }◊P⟺◻\mathrm{\neg }P$
  • $\mathrm{\neg }◻P⟺◊\mathrm{\neg }P$
  • $\mathrm{\neg }(P𝖴Q)⟺(P\wedge \mathrm{\neg }Q)𝖶(\mathrm{\neg }P\wedge \mathrm{\neg }Q)⟺\mathrm{\neg }P𝖱\mathrm{\neg }Q$
  • $\mathrm{\neg }(P𝖶Q)⟺(P\wedge \mathrm{\neg }Q)𝖴(\mathrm{\neg }P\wedge \mathrm{\neg }Q)$
  • $\mathrm{\neg }(P𝖱Q)⟺(\mathrm{\neg }P𝖴\mathrm{\neg }Q)$
• 멱등 법칙
  • $◊◊P⟺◊P$
  • $◻◻P⟺◻P$
  • $P𝖴(P𝖴Q)⟺P𝖴Q⟺(P𝖴Q)𝖴Q$
  • $P𝖶(P𝖶Q)⟺P𝖶Q⟺(P𝖶Q)𝖶Q$
  • $P𝖱(P𝖱Q)⟺P𝖱Q⟺(P𝖱Q)𝖱Q$
• 흡수 법칙
  • $◊◻◊P⟺◻◊P$
  • $◻◊◻P⟺◊◻P$
• 분배 법칙
  • $◯(P𝖴Q)⟺◯P𝖴◯Q$
  • $◯(P𝖶Q)⟺◯P𝖶◯Q$
  • $◯(P𝖱Q)⟺◯P𝖱◯Q$
  • $◊(P\vee Q)⟺◊P\vee ◊Q$
    • $◊(P\wedge Q)⟹◊P\wedge ◊Q$
  • $◻(P\wedge Q)⟺◻P\wedge ◻Q$
    • $◻(P\vee Q)⟸◻P\vee ◻Q$
• 전개 법칙
  • $◊P⟺P\vee ◯◊P$
  • $◻P⟺P\wedge ◯◻P$
  • $P𝖴Q⟺Q\vee (P\wedge ◯(P𝖴Q))$
  • $P𝖶Q⟺Q\vee (P\wedge ◯(P𝖶Q))$
  • $P𝖱Q⟺P\vee (Q\wedge ◯(P𝖱Q))$
  • $(X⟸(Q\vee (P\wedge ◯X)))⟹(X⟸P𝖴Q)$
  • $(X⟹(Q\vee (P\wedge ◯X)))⟹(X⟹P𝖶Q)$
• 기타 법칙
  • $◻P⟹\underset{n}{\underbrace{◯\cdots ◯}}P⟹◊P(n\in \{0,1,\dots \})$
  • $Q𝖱P\vee P𝖴Q⟹P𝖶Q$
  • $P𝖶Q⟺P𝖴Q\vee ◻Q$
  • $P𝖴Q⟺P𝖶Q\wedge ◊Q$
  • $P𝖶Q⟺(\mathrm{\neg }P\vee Q)𝖱(P\vee Q)$
  • $P𝖱Q⟺(\mathrm{\neg }P\wedge Q)𝖶(P\wedge Q)$

참고 문헌

• 틀:서적 인용