선형 시제 논리

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

통사론

선형 시제 논리의 논리식은 원자 명제의 유한 집합 $\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 {W}} Q=\lnot ((P\land \lnot Q)\operatorname {\mathsf {U}} {(}\lnot P\land \lnot Q))$
$P\operatorname {\mathsf {R}} Q=\lnot (\lnot P\operatorname {\mathsf {U}} \lnot Q)$
$\Diamond P=\top \operatorname {\mathsf {U}} P$
$\Box P=P\operatorname {\mathsf {W}} \bot =\bot \operatorname {\mathsf {R}} P$

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

$\bigcirc P$ : 바로 다음 번에 $P$ 가 참이다.
$\Diamond P$ : 결국/언젠가 $P$ 가 참이다.
$\Box P$ : 항상/언제나 $P$ 가 참이다.
$\Diamond \Box P$ : 언젠가부터 영원히 $P$ 가 참이다.
$\Box \Diamond P$ : 무한 개의 시점에서 $P$ 가 참이다.
$P\operatorname {\mathsf {U}} Q$ : 언젠가 $Q$ 가 참이기 바로 전까지 줄곧 $P$ 가 참이다.
$P\operatorname {\mathsf {W}} Q$ : $Q$ 가 참이기 바로 전까지 줄곧 $P$ 가 참이다.
$P\operatorname {\mathsf {R}} Q$ : $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 {U}} Q\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 {W}} Q\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 {R}} Q\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 {U}} Q$ 의 정의로부터 나머지 정의들을 유도할 수 있다.) 이에 따라, 선형 시제 논리식 $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 {U}} Q)\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 {W}} Q)\iff (P\land \lnot Q)\operatorname {\mathsf {U}} {(}\lnot P\land \lnot Q)$
- $\lnot (P\operatorname {\mathsf {R}} Q)\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 {U}} Q)\iff P\operatorname {\mathsf {U}} Q\iff (P\operatorname {\mathsf {U}} Q)\operatorname {\mathsf {U}} Q$
- $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$
- $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$
흡수 법칙
- $\Diamond \Box \Diamond P\iff \Box \Diamond P$
- $\Box \Diamond \Box P\iff \Diamond \Box P$
분배 법칙
- $\bigcirc (P\operatorname {\mathsf {U}} Q)\iff \bigcirc P\operatorname {\mathsf {U}} \bigcirc Q$
- $\bigcirc (P\operatorname {\mathsf {W}} Q)\iff \bigcirc P\operatorname {\mathsf {W}} \bigcirc Q$
- $\bigcirc (P\operatorname {\mathsf {R}} Q)\iff \bigcirc P\operatorname {\mathsf {R}} \bigcirc Q$
- $\Diamond (P\lor Q)\iff \Diamond P\lor \Diamond 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\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 {U}} Q\iff Q\lor (P\land \bigcirc (P\operatorname {\mathsf {U}} Q))$
- $P\operatorname {\mathsf {W}} Q\iff Q\lor (P\land \bigcirc (P\operatorname {\mathsf {W}} Q))$
- $P\operatorname {\mathsf {R}} Q\iff P\lor (Q\land \bigcirc (P\operatorname {\mathsf {R}} Q))$
- $(X\Longleftarrow (Q\lor (P\land \bigcirc X)))\implies (X\Longleftarrow P\operatorname {\mathsf {U}} Q)$
- $(X\implies (Q\lor (P\land \bigcirc X)))\implies (X\implies P\operatorname {\mathsf {W}} Q)$
기타 법칙
- $\Box P\implies \underbrace {\bigcirc \cdots \bigcirc } _{n}\,P\implies \Diamond P\qquad (n\in \{0,1,\dots \})$
- $Q\operatorname {\mathsf {R}} P\lor P\operatorname {\mathsf {U}} Q\implies P\operatorname {\mathsf {W}} Q$
- $P\operatorname {\mathsf {W}} Q\iff P\operatorname {\mathsf {U}} Q\lor \Box Q$
- $P\operatorname {\mathsf {U}} Q\iff P\operatorname {\mathsf {W}} Q\land \Diamond Q$
- $P\operatorname {\mathsf {W}} Q\iff (\lnot P\lor Q)\operatorname {\mathsf {R}} {(}P\lor Q)$
- $P\operatorname {\mathsf {R}} Q\iff (\lnot P\land Q)\operatorname {\mathsf {W}} {(}P\land Q)$