선형 시제 논리

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

## 통사론
선형 시제 논리의 논리식은 원자 명제의 유한 집합 \operatorname{AP}\sqcup\{\top,\bot\} 및 다음과 같은 논리 연산 기호들로부터 재귀적으로 정의된다.
* (명제 논리의 기호) <math>\land</math>, <math>\lor</math>, <math>\lnot</math>, <math>\implies</math> 등등
* (다음, ) \bigcirc
* (결국, ) \Diamond
* (항상, )  \Box
* (언틸, ) \mathsf U
* (약한 언틸, ) \mathsf W
* (풀기, ) \mathsf R
이들 기호는 다음과 같은 우선순위를 가진다.
* (일항 연산) \lnot, \bigcirc, \Diamond, \Box
* (명제 논리 밖의 이항 연산) \mathsf U, \mathsf W, \mathsf R
* (명제 논리의 이항 연산) \land, \lor, \implies
이들 기호는 \{\operatorname{AP},\land,\lnot,\bigcirc,\mathsf U\}로부터 다음과 같이 유도된다.
* P\lor Q=\lnot(\lnot P\land\lnot Q)
* P\implies Q=\lnot P\lor Q
* \top=p\implies p\qquad(p\in\operatorname{AP})
* \bot=\lnot\top
* P\operatorname\mathsf WQ=\lnot((P\land\lnot Q)\operatorname\mathsf U{(}\lnot P\land\lnot Q))
* P\operatorname\mathsf RQ=\lnot(\lnot P\operatorname\mathsf U\lnot Q)
* \Diamond P=\top\operatorname\mathsf UP
* \Box P=P\operatorname\mathsf W\bot=\bot\operatorname\mathsf RP
이들 기호는 다음과 같이 해석된다.
* \bigcirc P: 바로 다음 번에 P가 참이다.
* \Diamond P: 결국/언젠가 P가 참이다.
* \Box P: 항상/언제나 P가 참이다.
* \Diamond\Box P: 언젠가부터 영원히 P가 참이다.
* \Box\Diamond P: 무한 개의 시점에서 P가 참이다.
* P\operatorname\mathsf UQ:  언젠가 Q가 참이기 바로 전까지 줄곧 P가 참이다.
* P\operatorname\mathsf WQ: Q가 참이기 바로 전까지 줄곧 P가 참이다.
* P\operatorname\mathsf RQ: P가 참일 때까지 줄곧 Q가 참이다.

## 의미론
원자 명제 집합의 멱집합 위의 무한 열
:w=(w_0,w_1,w_2,\dots)\in(2^\operatorname{AP})^\omega
및 선형 시제 논리식 P가 주어졌다고 하자. 또한,
:w^j=(w_j,w_{j+1},w_{j+2},\dots)
와 같이 쓰자. 그렇다면, w가 P를 만족시킨다는 것은 w\models P와 같이 표기하며, 다음과 같이 재귀적으로 정의된다.
* w\models\top\iff\top
* w\models\bot\iff\bot
* w\models p\iff p\in w_0\qquad(p\in\operatorname{AP})
* w\models P\land Q\iff w\models P\land w\models Q
* w\models P\lor Q\iff w\models P\lor w\models Q
* w\models\lnot P\iff w\not\models P
* w\models P\implies Q\iff w\not\models P\lor w\models Q
* w\models\bigcirc P\iff w^1\models P
* w\models\Diamond P\iff\exists j\in\{0,1,\dots\}\colon w^j\models P
* w\models\Box P\iff\forall j\in\{0,1,\dots\}\colon w^j\models P
* w\models\Diamond\Box P\iff\exists j\in\{0,1,\dots\}\forall k\in\{j,j+1,\dots\}\colon w^k\models P
* w\models\Box\Diamond P\iff\forall j\in\{0,1,\dots\}\exists k\in\{j,j+1,\dots\}\colon w^k\models P
* w\models P\operatorname\mathsf UQ\iff\exists j\in\{0,1,\dots\}\colon w^0,\dots,w^{j-1}\models P\land w^j\models Q
* w\models P\operatorname\mathsf WQ\iff\exists j\in\{0,1,\dots,\infty\}\colon w^0,\dots,w^{j-1}\models P\land w^j\models Q
* w\models P\operatorname\mathsf RQ\iff\exists j\in\{0,1,\dots,\infty\}\colon w^0,\dots,w^j\models Q\land w^j\models P
(물론, w\models p(p\in\operatorname{AP}), w\models\lnot P, w\models P\land Q, w\models\bigcirc P, w\models P\operatorname\mathsf UQ의 정의로부터 나머지 정의들을 유도할 수 있다.) 이에 따라, 선형 시제 논리식 P는 의미론적으로 집합
:{\models}^{-1}(P)\subseteq(2^\operatorname{AP})^\omega
에 대응된다.

## 성질
선형 시제 논리식에 대하여, 다음과 같은 논리적 동치·함의 관계가 성립한다.
* 쌍대 법칙
** \lnot\bigcirc P\iff\bigcirc\lnot P
** \lnot\Diamond P\iff\Box\lnot P
** \lnot\Box P\iff\Diamond\lnot P
** \lnot(P\operatorname\mathsf UQ)\iff(P\land\lnot Q)\operatorname\mathsf W{(}\lnot P\land\lnot Q)
\iff\lnot P\operatorname\mathsf R\lnot Q
** \lnot(P\operatorname\mathsf WQ)\iff(P\land\lnot Q)\operatorname\mathsf U{(}\lnot P\land\lnot Q)
** \lnot(P\operatorname\mathsf RQ)\iff(\lnot P\operatorname\mathsf U\lnot Q)
* 멱등 법칙
** \Diamond\Diamond P\iff\Diamond P
** \Box\Box P\iff\Box P
** P\operatorname\mathsf U{(}P\operatorname\mathsf UQ)\iff P\operatorname\mathsf UQ\iff(P\operatorname\mathsf UQ)\operatorname\mathsf UQ
** P\operatorname\mathsf W{(}P\operatorname\mathsf WQ)\iff P\operatorname\mathsf WQ\iff(P\operatorname\mathsf WQ)\operatorname\mathsf WQ
** P\operatorname\mathsf R{(}P\operatorname\mathsf RQ)\iff P\operatorname\mathsf RQ\iff(P\operatorname\mathsf RQ)\operatorname\mathsf RQ
* 흡수 법칙
** \Diamond\Box\Diamond P\iff\Box\Diamond P
** \Box\Diamond\Box P\iff\Diamond\Box P
* 분배 법칙
** \bigcirc(P\operatorname\mathsf UQ)\iff\bigcirc P\operatorname\mathsf U\bigcirc Q
** \bigcirc(P\operatorname\mathsf WQ)\iff\bigcirc P\operatorname\mathsf W\bigcirc Q
** \bigcirc(P\operatorname\mathsf RQ)\iff\bigcirc P\operatorname\mathsf R\bigcirc Q
** \Diamond(P\lor Q)\iff\Diamond P\lor\Diamond Q
*** \Diamond(P\land Q)\implies\Diamond P\land\Diamond Q
** \Box(P\land Q)\iff\Box P\land\Box Q
*** \Box(P\lor Q)\Longleftarrow\Box P\lor\Box Q
* 전개 법칙
** \Diamond P\iff P\lor\bigcirc\Diamond P
** \Box P\iff P\land\bigcirc\Box P
** P\operatorname\mathsf UQ\iff Q\lor(P\land\bigcirc(P\operatorname\mathsf UQ))
** P\operatorname\mathsf WQ\iff Q\lor(P\land\bigcirc(P\operatorname\mathsf WQ))
** P\operatorname\mathsf RQ\iff P\lor(Q\land\bigcirc(P\operatorname\mathsf RQ))
** (X\Longleftarrow(Q\lor(P\land\bigcirc X)))\implies(X\Longleftarrow P\operatorname\mathsf UQ)
** (X\implies(Q\lor(P\land\bigcirc X)))\implies(X\implies P\operatorname\mathsf WQ)
* 기타 법칙
** \Box P\implies\underbrace{\bigcirc\cdots\bigcirc}_n\,P\implies \Diamond P\qquad(n\in\{0,1,\dots\})
** Q\operatorname\mathsf RP\lor P\operatorname\mathsf UQ\implies P\operatorname\mathsf WQ
** P\operatorname\mathsf WQ\iff P\operatorname\mathsf UQ\lor\Box Q
** P\operatorname\mathsf UQ\iff P\operatorname\mathsf WQ\land\Diamond Q
** P\operatorname\mathsf WQ\iff(\lnot P\lor Q)\operatorname\mathsf R{(}P\lor Q)
** P\operatorname\mathsf RQ\iff(\lnot P\land Q)\operatorname\mathsf W{(}P\land Q)

## 각주

## 참고 문헌
* 

분류:1977년 도입
분류:시간 논리