선형 시제 논리

논리학에서 **선형 시제 논리**(線型時制論理, linear temporal logic, 약자 LTL)는 선형 이산 시간에 대한 여러 가지 양상을 갖춘, 시제 논리의 하나이다. PTL(Propositional temporal logic)이라고도 한다.page=46
# 통사론
선형 시제 논리의 논리식은 원자 명제의 유한 집합 \operatorname{AP}\sqcup\\{\top,\bot\\} 및 다음과 같은 논리 연산 기호들로부터 재귀적으로 정의된다. * (명제 논리의 기호) \land, \lor, \lnot, \implies 등등 * (다음, next) \bigcirc * (결국, eventually) \Diamond * (항상, always) \Box * (언틸, until) \mathsf U * (약한 언틸, weak until) \mathsf W * (풀기, release) \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)