선형 시제 논리 문서 원본 보기

{{위키데이터 속성 추적}}
[[논리학]]에서 '''선형 시제 논리'''(線型時制論理, {{llang|en|linear temporal logic}}, 약자 LTL)는 선형 이산 시간에 대한 여러 가지 [[양상 논리|양상]]을 갖춘, [[시제 논리]]의 하나이다. PTL(Propositional temporal logic)이라고도 한다.<ref name="Gabbay2003">{{서적 인용|author1=[[Dov M. Gabbay]]|author2= A. Kurucz|author3= F. Wolter|author4= M. Zakharyaschev|title=Many-dimensional modal logics: theory and applications|url=https://books.google.com/books?id=P8jZwiExZYEC&pg=PA46|year=2003|publisher=Elsevier|isbn=978-0-444-50826-3|page=46}}</ref>

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

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

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

== 각주 ==
{{각주}}

== 참고 문헌 ==
* {{서적 인용
|성1=Baier
|이름1=Christel
|성2=Katoen
|이름2=Joost-Pieter
|제목=Principles of Model Checking
|언어=en
|출판사=The MIT Press
|날짜=2008
|isbn=978-0-262-02649-9
}}

{{논리학}}
[[분류:1977년 도입]]
[[분류:시간 논리]]