선형 시제 논리

1. 개요

선형 시제 논리(LTL)는 미래에 대한 진술을 표현하기 위한 시제 논리의 한 유형이다. LTL은 원자 명제, 논리 연산자, 다음(next, O), 결국(eventually, ⋄), 항상(always, □), 언틸(until, U) 등의 시간 양상 연산자를 사용하여 공식을 구성한다. LTL은 다양한 분야에서 시스템의 속성을 명세하고 검증하는 데 사용되며, 모델 검사 및 형식 검증에 널리 활용된다. LTL 공식은 PSPACE-완전 문제이며, 시스템이 따라야 하는 제약 조건, 사양 또는 프로세스를 표현하는 데 사용된다.

2. 통사론

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

2.1. 기본 연산자

명제 변수 AP, 논리 연산자 ¬ 및 ∨, 그리고 시간 양상 연산자 X (일부 문헌에서는 O 또는 N을 사용)와 U로 구성된다.

* 만약 이면, p는 LTL 공식이다.
* 만약 와 가 LTL 공식이면 , 그리고 는 LTL 공식이다.

X는 "다음(next)"으로 읽고, U는 "언틸(until, ~까지)"로 읽는다.
이러한 기본 연산자 외에도, LTL 공식을 간결하게 작성하기 위해 기본 연산자를 사용하여 정의된 추가 논리 및 시간 연산자가 있다. 추가 논리 연산자는 ∧, →, ↔, true, 그리고 false이다.

다음은 추가 시간 연산자이다.

* G는 항상(globally)
* F는 마침내(finally)
* R는 릴리즈(release)
* W는 약한 언틸(weak until)
* M은 강력한 릴리즈(mighty release)

처음 3개의 연산자(N, G, F)는 단항 연산이다. $\backslash phi$가 논리식이라면, N $\backslash phi$도 논리식이다. U와 R 연산자는 이항 연산이다. $\backslash phi$와 $\backslash psi$가 논리식이라면, $\backslash phi$ U $\backslash psi$도 논리식이다.

2.2. 확장 연산자

기본 연산자를 조합하여 추가적인 시간 양상 연산자를 정의할 수 있다.

일부 저자는 정지 조건이 발생할 필요가 없는 (release와 유사한) 의미를 가진 weak until 이진 연산자 W를 정의한다. U와 R 모두 weak until을 사용하여 정의할 수 있으므로 유용하다.

* ψ W φ ≡ (ψ U φ) ∨ G ψ ≡ ψ U (φ ∨ G ψ) ≡ φ R (φ ∨ ψ)
* ψ U φ ≡ Fφ ∧ (ψ W φ)
* ψ R φ ≡ φ W (φ ∧ ψ)

strong release 이진 연산자 M은 weak until의 이중 연산자이다. until 연산자와 유사하게 정의되어 release 조건이 어떤 시점에 반드시 참이 되도록 한다. 따라서 release 연산자보다 더 강력하다.

* ψ M φ ≡ ¬(¬ψ W ¬φ) ≡ (ψ R φ) ∧ F ψ ≡ ψ R (φ ∧ F ψ) ≡ φ U (ψ ∧ φ)

3. 의미론

선형 시제 논리 공식은 '만족' 관계를 통해 의미를 부여받는다. 만족성은 *AP* 내 변수들의 진리값에 대한 무한 시퀀스(ω-단어, 크립키 구조의 경로)를 통해 정의된다.

원자 명제 집합의 멱집합 위의 무한 열
:$w=(w\_0,w\_1,w\_2,\backslash dots)\backslash in(2^\backslash operatorname\{AP\})^\backslash omega$
및 선형 시제 논리식 $P$가 주어졌다고 하자.
:$w^j=(w\_j,w\_\{j+1\},w\_\{j+2\},\backslash dots)$
와 같이 쓰자. 그렇다면, $w$가 $P$를 만족시킨다는 것은 $w\backslash models\; P$와 같이 표기하며, 다음과 같이 재귀적으로 정의된다.

* $w\backslash models\backslash top\backslash iff\backslash top$
* $w\backslash models\backslash bot\backslash iff\backslash bot$
* $w\backslash models\; p\backslash iff\; p\backslash in\; w\_0\backslash qquad(p\backslash in\backslash operatorname\{AP\})$
* $w\backslash models\; P\backslash land\; Q\backslash iff\; w\backslash models\; P\backslash land\; w\backslash models\; Q$
* $w\backslash models\; P\backslash lor\; Q\backslash iff\; w\backslash models\; P\backslash lor\; w\backslash models\; Q$
* $w\backslash models\backslash lnot\; P\backslash iff\; w\backslash not\backslash models\; P$
* $w\backslash models\; P\backslash implies\; Q\backslash iff\; w\backslash not\backslash models\; P\backslash lor\; w\backslash models\; Q$
* $w\backslash models\backslash bigcirc\; P\backslash iff\; w^1\backslash models\; P$
* $w\backslash models\backslash Diamond\; P\backslash iff\backslash exists\; j\backslash in\backslash \{0,1,\backslash dots\backslash \}\backslash colon\; w^j\backslash models\; P$
* $w\backslash models\backslash Box\; P\backslash iff\backslash forall\; j\backslash in\backslash \{0,1,\backslash dots\backslash \}\backslash colon\; w^j\backslash models\; P$
* $w\backslash models\backslash Diamond\backslash Box\; P\backslash iff\backslash exists\; j\backslash in\backslash \{0,1,\backslash dots\backslash \}\backslash forall\; k\backslash in\backslash \{j,j+1,\backslash dots\backslash \}\backslash colon\; w^k\backslash models\; P$
* $w\backslash models\backslash Box\backslash Diamond\; P\backslash iff\backslash forall\; j\backslash in\backslash \{0,1,\backslash dots\backslash \}\backslash exists\; k\backslash in\backslash \{j,j+1,\backslash dots\backslash \}\backslash colon\; w^k\backslash models\; P$
* $w\backslash models\; P\backslash operatorname\backslash mathsf\; UQ\backslash iff\backslash exists\; j\backslash in\backslash \{0,1,\backslash dots\backslash \}\backslash colon\; w^0,\backslash dots,w^\{j-1\}\backslash models\; P\backslash land\; w^j\backslash models\; Q$
* $w\backslash models\; P\backslash operatorname\backslash mathsf\; WQ\backslash iff\backslash exists\; j\backslash in\backslash \{0,1,\backslash dots,\backslash infty\backslash \}\backslash colon\; w^0,\backslash dots,w^\{j-1\}\backslash models\; P\backslash land\; w^j\backslash models\; Q$
* $w\backslash models\; P\backslash operatorname\backslash mathsf\; RQ\backslash iff\backslash exists\; j\backslash in\backslash \{0,1,\backslash dots,\backslash infty\backslash \}\backslash colon\; w^0,\backslash dots,w^j\backslash models\; Q\backslash land\; w^j\backslash models\; P$

(물론, $w\backslash models\; p$($p\backslash in\backslash operatorname\{AP\}$), $w\backslash models\backslash lnot\; P$, $w\backslash models\; P\backslash land\; Q$, $w\backslash models\backslash bigcirc\; P$, $w\backslash models\; P\backslash operatorname\backslash mathsf\; UQ$의 정의로부터 나머지 정의들을 유도할 수 있다.) 이에 따라, 선형 시제 논리식 $P$는 의미론적으로 집합
:$\{\backslash models\}^\{-1\}(P)\backslash subseteq(2^\backslash operatorname\{AP\})^\backslash omega$
에 대응된다.

ω-단어 w가 LTL 공식 를 만족시킨다는 것은, w ⊨ 를 의미한다.
로 정의된 ω-언어 L()는 {w | w ⊨ }이며, 이는 를 만족시키는 ω-단어들의 집합이다.
공식 는 만족 가능하다는 것은, w ⊨ 를 만족하는 ω-단어 w가 존재한다는 의미이다.
공식 가 유효하다는 것은, 알파벳 2^AP에 대한 모든 ω-단어 w에 대해, w ⊨ 가 성립한다는 의미이다.

추가적인 논리 연산자는 다음과 같이 정의된다.
* ∧ ≡ ¬(¬ ∨ ¬)
* → ≡ ¬ ∨
* ↔ ≡ ( → ) ∧ ( → )
* true ≡ p ∨ ¬p, 여기서 p ∈ AP
* false ≡ ¬true
추가적인 시간 연산자 R, F, G는 다음과 같이 정의된다.
* R ≡ ¬(¬ U ¬) (가 참이 될 때까지 (그리고 그 시점까지) 가 참으로 유지된다. 만약 가 절대로 참이 되지 않으면, 는 영원히 참으로 유지되어야 한다. releases .)
* (결국 가 참이 된다)
* G ≡ false R ≡ ¬F ¬ (는 항상 참으로 유지된다)

다음의 항등식이 성립하므로, 연산자의 종류를 줄일 수 있다:
*F $\backslash phi$ = true U $\backslash phi$
*G $\backslash phi$ = false R $\backslash phi$ = $\backslash neg$ F $\backslash neg$$\backslash phi$
*$\backslash psi$ R $\backslash phi$ = $\backslash neg$($\backslash neg$$\backslash psi$ U $\backslash neg$$\backslash phi$)

3.1. 만족 관계 (⊨)

LTL 공식은 크립키 구조의 경로상에 있는 단어(ω-단어)로 만족될 수 있다. ω-단어 *w* = a₀,a₁,a₂,... 와 LTL 공식 ψ에 대해, *w* ⊨ ψ 는 *w*가 ψ를 만족시킨다는 것을 의미한다. *w*(*i*) = *a_i*이고, *w*ⁱ = *a_i*,*a_i+1*,...는 *w*의 접미사이다.

만족 관계 ⊨는 다음과 같이 재귀적으로 정의된다.

* *w* ⊨ *p* (만약 *p* ∈ *w*(0) 이면)
* *w* ⊨ ¬ψ (만약 *w* ⊭ ψ 이면)
* *w* ⊨ φ ∨ ψ (만약 *w* ⊨ φ 이거나 *w* ⊨ ψ 이면)
* *w* ⊨ X ψ (만약 *w*¹ ⊨ ψ 이면)
* *w* ⊨ φ U ψ (만약 어떤 *i* ≥ 0에 대해 *w*^*i* ⊨ ψ 이고, 모든 0 ≤ *k* < *i*에 대해 *w*^*k* ⊨ φ 이면)

ω-단어 *w*가 LTL 공식 ψ를 만족시킨다는 것은 *w* ⊨ ψ임을 의미하며, ψ로 정의된 ω-언어 *L*(ψ)는 {*w* | *w* ⊨ ψ}이며, 이는 ψ를 만족시키는 ω-단어들의 집합이다. 공식 ψ는 *w* ⊨ ψ를 만족하는 ω-단어 *w*가 존재하면 만족 가능하고, 알파벳 2^AP에 대한 모든 ω-단어 *w*에 대해 *w* ⊨ ψ가 성립하면 유효하다.

추가적인 논리 연산자(∧, →, ↔, true, false)와 시간 연산자 (R, F, G)는 기본 연산자를 통해 정의된 의미와 동치이다.

4. 성질

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

* 쌍대 법칙
:* ¬XP ≡ X¬P
:* ¬FP ≡ G¬P
:* ¬GP ≡ F¬P
:* ¬(P U Q) ≡ (P ∧ ¬Q) W (¬P ∧ ¬Q) ≡ ¬P R ¬Q
:* ¬(P W Q) ≡ (P ∧ ¬Q) U (¬P ∧ ¬Q)
:* ¬(P R Q) ≡ (¬P U ¬Q)
* 멱등 법칙
:* F F P ≡ F P
:* G G P ≡ G P
:* P U (P U Q) ≡ P U Q ≡ (P U Q) U Q
:* P W (P W Q) ≡ P W Q ≡ (P W Q) W Q
:* P R (P R Q) ≡ P R Q ≡ (P R Q) R Q
* 흡수 법칙
:* F G F P ≡ G F P
:* G F G P ≡ F G P
* 분배 법칙
:* X(P U Q) ≡ XP U XQ
:* X(P W Q) ≡ XP W XQ
:* X(P R Q) ≡ XP R XQ
:* F(P ∨ Q) ≡ FP ∨ FQ
:* F(P ∧ Q) → FP ∧ FQ
:* G(P ∧ Q) ≡ GP ∧ GQ
:* G(P ∨ Q) ← GP ∨ GQ
* 전개 법칙
:* FP ≡ P ∨ X FP
:* GP ≡ P ∧ X GP
:* P U Q ≡ Q ∨ (P ∧ X(P U Q))
:* P W Q ≡ Q ∨ (P ∧ X(P W Q))
:* P R Q ≡ P ∨ (Q ∧ X(P R Q))
:* (X ← (Q ∨ (P ∧ XX))) → (X ← P U Q)
:* (X → (Q ∨ (P ∧ XX))) → (X → P W Q)
* 기타 법칙
:* GP → X...XP → FP (n ∈ {0, 1, ...})
:* Q R P ∨ P U Q → P W Q
:* P W Q ≡ P U Q ∨ GQ
:* P U Q ≡ P W Q ∧ FQ
:* P W Q ≡ (¬P ∨ Q) R (P ∨ Q)
:* P R Q ≡ (¬P ∧ Q) W (P ∧ Q)

φ, ψ, ρ를 선형 시제 논리 공식이라고 하면, 일반적인 논리 연산자에 대한 표준 동치를 확장하는 유용한 동치 관계는 다음과 같다.

모든 선형 시제 논리 수식은 부정 정규 형식으로 변환할 수 있다. 부정 정규 형식에서는 모든 부정 기호(¬)가 원자 명제 앞에만 나타나고, 다른 논리 연산자 참, 거짓, ∧, ∨ 만 나타날 수 있으며, 시간 연산자 X, U, R 만 나타날 수 있다. 부정 전파에 대한 위의 동치성을 사용하여 정규 형식을 유도할 수 있다. 이 정규 형식은 LTL의 기본적인 연산자가 아닌 R, 참, 거짓, ∧ 이 수식에 나타나는 것을 허용한다. 부정 정규 형식으로의 변환은 수식의 길이를 증가시키지 않으며, LTL 수식을 뷔치 오토마톤으로 변환하는 데 유용하다.

4.1. 주요 동치 관계

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

* 쌍대 법칙
:* ¬XP ≡ X¬P
:* ¬FP ≡ G¬P
:* ¬GP ≡ F¬P
:* ¬(P U Q) ≡ (P ∧ ¬Q) W (¬P ∧ ¬Q) ≡ ¬P R ¬Q
:* ¬(P W Q) ≡ (P ∧ ¬Q) U (¬P ∧ ¬Q)
:* ¬(P R Q) ≡ (¬P U ¬Q)
* 멱등 법칙
:* F F P ≡ F P
:* G G P ≡ G P
:* P U (P U Q) ≡ P U Q ≡ (P U Q) U Q
:* P W (P W Q) ≡ P W Q ≡ (P W Q) W Q
:* P R (P R Q) ≡ P R Q ≡ (P R Q) R Q
* 흡수 법칙
:* F G F P ≡ G F P
:* G F G P ≡ F G P
* 분배 법칙
:* X(P U Q) ≡ XP U XQ
:* X(P W Q) ≡ XP W XQ
:* X(P R Q) ≡ XP R XQ
:* F(P ∨ Q) ≡ FP ∨ FQ
:* F(P ∧ Q) → FP ∧ FQ
:* G(P ∧ Q) ≡ GP ∧ GQ
:* G(P ∨ Q) ← GP ∨ GQ
* 전개 법칙
:* FP ≡ P ∨ X FP
:* GP ≡ P ∧ X GP
:* P U Q ≡ Q ∨ (P ∧ X(P U Q))
:* P W Q ≡ Q ∨ (P ∧ X(P W Q))
:* P R Q ≡ P ∨ (Q ∧ X(P R Q))
:* (X ← (Q ∨ (P ∧ XX))) → (X ← P U Q)
:* (X → (Q ∨ (P ∧ XX))) → (X → P W Q)
* 기타 법칙
:* GP → X...XP → FP (n ∈ {0, 1, ...})
:* Q R P ∨ P U Q → P W Q
:* P W Q ≡ P U Q ∨ GQ
:* P U Q ≡ P W Q ∧ FQ
:* P W Q ≡ (¬P ∨ Q) R (P ∨ Q)
:* P R Q ≡ (¬P ∧ Q) W (P ∧ Q)

φ, ψ, ρ를 LTL 공식이라고 하면, 일반적인 논리 연산자에 대한 표준 동치를 확장하는 유용한 동치 관계는 다음과 같다.

모든 선형 시제 논리 수식은 부정 정규 형식으로 변환할 수 있다. 부정 정규 형식에서는 모든 부정 기호(¬)가 원자 명제 앞에만 나타나고, 다른 논리 연산자 참, 거짓, ∧, ∨ 만 나타날 수 있으며, 시간 연산자 X, U, R 만 나타날 수 있다. 부정 전파에 대한 위의 동치성을 사용하여 정규 형식을 유도할 수 있다. 이 정규 형식은 LTL의 기본적인 연산자가 아닌 R, 참, 거짓, ∧ 이 수식에 나타나는 것을 허용한다. 부정 정규 형식으로의 변환은 수식의 길이를 증가시키지 않으며, LTL 수식을 뷔치 오토마톤으로 변환하는 데 유용하다.

5. 다른 논리와의 관계

LTL은 단항 1차 논리 FO[<]와 동등하며, 이는 캄프의 정리로 알려져 있다. 또는 별 없는 언어와도 같다. 계산 트리 논리(CTL)와 선형 시제 논리 (LTL)는 모두 CTL*의 하위 집합이지만 서로 비교할 수 없다. CTL 공식으로 LTL 공식 F(G p)에 의해 정의된 언어를 정의할 수 없고, 반대로 LTL 공식으로 CTL 공식 AG( p → (EXq ∧ EX¬q) ) 또는 AG(EF(p))에 의해 정의된 언어를 정의할 수 없다. LTL은 후자(successor, 페아노 공리 참조)와 "작다" 관계에 대한 1차 술어 논리 FO[S, <]와 등가이다. 또한, 클레이니 스타가 없는 정규 표현식이나 루프 복잡도가 0인 결정적 유한 오토마톤도 LTL과 등가이다.

6. 계산 복잡도

모델 검사 및 LTL 공식에 대한 만족 가능성은 PSPACE-완전 문제이다. LTL 합성 및 LTL 승리 조건에 대한 게임 검증 문제는 2EXPTIME-완전 문제이다.

7. 응용

LTL 공식은 시스템이 따라야 하는 제약 조건, 사양 또는 프로세스를 표현하는 데 일반적으로 사용된다. 모델 검사 분야는 시스템이 주어진 사양을 충족하는지 공식적으로 확인하는 것을 목표로 한다. 오토마타 이론 모델 검사의 경우, 관심 있는 시스템과 사양 모두 별도의 유한 상태 기계, 즉 오토마타로 표현된 다음 비교하여 시스템이 지정된 속성을 가질 것이라고 보장되는지 평가한다. 컴퓨터 과학에서 이러한 유형의 모델 검사는 알고리즘이 올바르게 구조화되었는지 확인하는 데 자주 사용된다.

무한 시스템 실행에 대한 LTL 사양을 확인하기 위해, 모델과 동일한 (모델인 경우에만 ω-단어를 허용) Büchi 오토마톤과 속성의 부정과 동일한 (부정된 속성을 만족하는 경우에만 ω-단어를 허용) 오토마톤을 구하는 것이 일반적인 기법이다(선형 시간 논리에서 Büchi 오토마톤으로). 이 경우, 두 오토마톤에서 허용되는 ω-단어 집합에 중복이 있으면 모델이 원하는 속성을 위반하는 일부 동작을 허용함을 의미한다. 중복이 없으면 모델에서 허용하는 속성 위반 동작이 없다. 공식적으로, 두 비결정적 Büchi 오토마톤의 교집합이 비어 있는 경우에만 모델이 지정된 속성을 만족한다.

선형 시간 논리를 사용하여 표현할 수 있는 속성은 크게 두 가지 유형이 있다. 안전 속성은 일반적으로 '나쁜 일이 절대 일어나지 않는다'(G¬ϕ)를 나타내는 반면, 생존성 속성은 '좋은 일이 계속 일어난다'(GFψ 또는 G(ϕ →Fψ))를 나타낸다. 예를 들어, 안전 속성은 자율 주행 로버가 절벽 위로 운전하지 않거나 소프트웨어 제품이 잘못된 비밀번호로 성공적인 로그인을 허용하지 않도록 요구할 수 있다. 생존성 속성은 로버가 항상 데이터 샘플을 계속 수집하거나 소프트웨어 제품이 텔레메트리 데이터를 반복적으로 전송하도록 요구할 수 있다.

더 일반적으로, 안전 속성은 모든 반례에 유한 접두사가 있어, 무한 경로로 확장하더라도 여전히 반례인 속성이다. 반면에 생존성 속성의 경우, 모든 유한 경로는 공식을 만족하는 무한 경로로 확장할 수 있다.

선형 시간 논리의 응용 분야 중 하나는 선호도 기반 계획의 목적으로 계획 도메인 정의 언어에서 선호도를 지정하는 것이다.

7.1. 모델 검사

LTL 공식은 시스템이 따라야 하는 제약 조건, 사양 또는 프로세스를 표현하는 데 일반적으로 사용된다. 모델 검사 분야는 시스템이 주어진 사양을 충족하는지 공식적으로 확인하는 것을 목표로 한다. 오토마타 이론 모델 검사의 경우, 관심 있는 시스템과 사양 모두 별도의 유한 상태 기계, 즉 오토마타로 표현된 다음 비교하여 시스템이 지정된 속성을 가질 것이라고 보장되는지 평가한다. 컴퓨터 과학에서 이러한 유형의 모델 검사는 알고리즘이 올바르게 구조화되었는지 확인하는 데 자주 사용된다.

무한 시스템 실행에 대한 LTL 사양을 확인하기 위해, 모델과 동일한 (모델인 경우에만 ω-단어를 허용) Büchi 오토마톤과 속성의 부정과 동일한 (부정된 속성을 만족하는 경우에만 ω-단어를 허용) 오토마톤을 구하는 것이 일반적인 기법이다(선형 시간 논리에서 Büchi 오토마톤으로). 이 경우, 두 오토마톤에서 허용되는 ω-단어 집합에 중복이 있으면 모델이 원하는 속성을 위반하는 일부 동작을 허용함을 의미한다. 중복이 없으면 모델에서 허용하는 속성 위반 동작이 없다. 공식적으로, 두 비결정적 Büchi 오토마톤의 교집합이 비어 있는 경우에만 모델이 지정된 속성을 만족한다.

선형 시간 논리를 사용하여 표현할 수 있는 속성은 크게 두 가지 유형이 있다. 안전 속성은 일반적으로 '나쁜 일이 절대 일어나지 않는다'(G¬ϕ)를 나타내는 반면, 생존성 속성은 '좋은 일이 계속 일어난다'(GFψ 또는 G(ϕ →Fψ))를 나타낸다. 예를 들어, 안전 속성은 자율 주행 로버가 절벽 위로 운전하지 않거나 소프트웨어 제품이 잘못된 비밀번호로 성공적인 로그인을 허용하지 않도록 요구할 수 있다. 생존성 속성은 로버가 항상 데이터 샘플을 계속 수집하거나 소프트웨어 제품이 텔레메트리 데이터를 반복적으로 전송하도록 요구할 수 있다.

더 일반적으로, 안전 속성은 모든 반례에 유한 접두사가 있어, 무한 경로로 확장하더라도 여전히 반례인 속성이다. 반면에 생존성 속성의 경우, 모든 유한 경로는 공식을 만족하는 무한 경로로 확장할 수 있다.

선형 시간 논리의 응용 분야 중 하나는 선호도 기반 계획의 목적으로 계획 도메인 정의 언어에서 선호도를 지정하는 것이다.

7.2. 형식 검증

LTL 공식은 시스템이 따라야 하는 제약 조건, 사양 또는 프로세스를 표현하는 데 일반적으로 사용된다. 모델 검사 분야는 시스템이 주어진 사양을 충족하는지 공식적으로 확인하는 것을 목표로 한다. 오토마타 이론 모델 검사의 경우, 관심 있는 시스템과 사양 모두 별도의 유한 상태 기계, 즉 오토마타로 표현된 다음 비교하여 시스템이 지정된 속성을 가질 것이라고 보장되는지 평가한다.

무한 시스템 실행에 대한 LTL 사양을 확인하기 위해, 모델과 동일한 (모델인 경우에만 ω-단어를 허용) Büchi 오토마톤과 속성의 부정과 동일한 (부정된 속성을 만족하는 경우에만 ω-단어를 허용) 오토마톤을 구하는 것이 일반적인 기법이다. 이 경우, 두 오토마톤에서 허용되는 ω-단어 집합에 중복이 있으면 모델이 원하는 속성을 위반하는 일부 동작을 허용함을 의미한다. 중복이 없으면 모델에서 허용하는 속성 위반 동작이 없다. 공식적으로, 두 비결정적 Büchi 오토마톤의 교집합이 비어 있는 경우에만 모델이 지정된 속성을 만족한다.

LTL을 사용하여 표현할 수 있는 속성은 크게 두 가지 유형이 있다. 안전 속성은 일반적으로 '나쁜 일이 절대 일어나지 않는다'(G¬ϕ)를 나타내는 반면, 생존성 속성은 '좋은 일이 계속 일어난다'(GFψ 또는 G(ϕ →Fψ))를 나타낸다. 안전 속성은 모든 반례에 유한 접두사가 있어, 무한 경로로 확장하더라도 여전히 반례인 속성이다. 반면에 생존성 속성의 경우, 모든 유한 경로는 공식을 만족하는 무한 경로로 확장할 수 있다.

선형 시간 논리의 응용 분야 중 하나는 선호도 기반 계획의 목적으로 계획 도메인 정의 언어에서 선호도를 지정하는 것이다.

7.3. 기타 응용

선형 시제 논리(LTL)는 선호도 기반 계획에서 계획 도메인 정의 언어의 선호도를 지정하는데 사용될 수 있다. LTL 공식은 시스템이 따라야 하는 제약 조건, 사양 또는 프로세스를 표현하는 데 일반적으로 사용된다. 모델 검사 분야는 시스템이 주어진 사양을 충족하는지 공식적으로 확인하는 것을 목표로 한다. 오토마타 이론 모델 검사의 경우, 관심 있는 시스템과 사양 모두 별도의 유한 상태 기계, 즉 오토마타로 표현된 다음 비교하여 시스템이 지정된 속성을 가질 것이라고 보장되는지 평가한다.

선형 시간 논리를 사용하여 표현할 수 있는 속성은 크게 안전 속성과 생존성 속성의 두 가지 유형이 있다. 안전 속성은 일반적으로 '나쁜 일이 절대 일어나지 않는다'는 것을 나타내고, 생존성 속성은 '좋은 일이 계속 일어난다'는 것을 나타낸다.