선형 시제 논리

"오늘의AI위키"는 AI 기술로 일관성 있고 체계적인 최신 지식을 제공하는 혁신 플랫폼입니다.
"오늘의AI위키"의 AI를 통해 더욱 풍부하고 폭넓은 지식 경험을 누리세요.

1. 개요
2. 통사론
- 2.1. 기본 연산자
- 2.2. 확장 연산자
3. 의미론
- 3.1. 만족 관계 (⊨)
4. 성질
- 4.1. 주요 동치 관계
5. 다른 논리와의 관계
6. 계산 복잡도
7. 응용
참조

1. 개요

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

더 읽어볼만한 페이지

시간 논리 - 계산 트리 논리
계산 트리 논리(CTL)는 에드먼드 M. 클라크와 E. 앨런 에머슨이 제안한 논리 체계로, 논리 연산자, 경로 연산자(A, E), 상태 연산자(X, G, F, U, W)를 조합하여 시스템 상태 변화를 기술하며 모델 검사에서 효율적인 계산이 가능하다.
시간 논리 - 크립키 구조
크립키 구조는 가능한 세계의 집합, 세계 간의 접근 관계, 각 세계에서 원자 명제의 진리값을 할당하는 평가 함수로 구성되어 양상 논리의 의미론을 정의하며, 가능성과 필연성과 같은 모달 논리의 핵심 개념을 이해하는 데 기여한다.
1977년 도입 - 아타리 2600
아타리 2600은 1977년 출시되어 1970년대 후반과 1980년대 초반 비디오 게임 시장을 선도했으며, 다양한 게임 카트리지를 지원하고 서드 파티 게임 개발을 가능하게 하여 비디오 게임 위기를 겪었음에도 콘솔 및 비디오 게임의 대명사가 되었다.
1977년 도입 - 컬러 TV 게임
컬러 TV 게임은 닌텐도가 1977년부터 1980년까지 발매한 전용 게임기 시리즈로, 특정 게임이나 게임 모음집을 내장하고 가정용 TV에 연결하여 즐길 수 있도록 설계되었으며, 닌텐도가 비디오 게임 시장에 진출하고 저가형 하드웨어 판매 전략을 확립하는 데 기여했다.

선형 시제 논리
개요
유형	모달 논리
분야	논리학, 컴퓨터 과학
기반	시제 논리
개발자	아미르 프누엘리
발표일	1977년
특징
표현력	1차 논리와 동일
사용 목적	컴퓨터 시스템의 행동 양식 검증
추가 정보
적용 분야	병행 프로그램
참고	계산 트리 논리

2. 통사론

원자 명제의 유한 집합 $\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$ 가 참이다.

2. 1. 기본 연산자

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

만약 이면, ''p''는 LTL 공식이다.
만약 와 가 LTL 공식이면 , ∨ , '''X''' }}, 그리고 '''U''' }}는 LTL 공식이다.^[7]

'''X'''는 "다음(ne'''x'''t)"으로 읽고, '''U'''는 "언틸('''u'''ntil, ~까지)"로 읽는다.^[7]

이러한 기본 연산자 외에도, LTL 공식을 간결하게 작성하기 위해 기본 연산자를 사용하여 정의된 추가 논리 및 시간 연산자가 있다. 추가 논리 연산자는 ∧, →, ↔, '''true''', 그리고 '''false'''이다.

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

'''G'''는 항상('''g'''lobally)
'''F'''는 마침내('''f'''inally)
'''R'''는 릴리즈('''r'''elease)
'''W'''는 약한 언틸('''w'''eak until)
'''M'''은 강력한 릴리즈('''m'''ighty release)

처음 3개의 연산자('''N''', '''G''', '''F''')는 단항 연산이다.

\phi

가 논리식이라면, '''N'''

\phi

도 논리식이다. '''U'''와 '''R''' 연산자는 이항 연산이다.

\phi

와

\psi

가 논리식이라면,

\phi

'''U'''

\psi

도 논리식이다.

2. 2. 확장 연산자

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

일부 저자는 정지 조건이 발생할 필요가 없는 (release와 유사한) 의미를 가진 ''weak until'' 이진 연산자 '''W'''를 정의한다.^[8] '''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''' (''ψ'' ∧ ''φ'')

텍스트	기호	설명	다이어그램
단항 연산자:
X φ	$\bigcirc \varphi$	neXt: 다음 상태에서 φ가 참이어야 한다.	LTL 다음 연산자
F φ	$\Diamond \varphi$	Finally: φ는 결국 (후속 경로 어딘가에서) 참이어야 한다.	LTL 결국 연산자
G φ	$\Box \varphi$	Globally: φ는 전체 후속 경로에서 참이어야 한다.	LTL 항상 연산자
이항 연산자:
ψ U φ	$\psi\;\mathcal{U}\,\varphi$	Until: φ가 참이 될 때까지 ψ가 참이어야 하며, 이는 현재 또는 미래의 위치에서 참이어야 한다.	LTL until 연산자
ψ R φ	$\psi\;\mathcal{R}\,\varphi$	Release: ψ가 처음으로 참이 되는 시점까지, 그리고 그 시점을 포함하여, φ가 참이어야 한다. ψ가 절대 참이 되지 않으면 φ는 영원히 참으로 유지되어야 한다.	LTL release 연산자 (중지)
ψ W φ	$\psi\;\mathcal{W}\,\varphi$	Weak until: φ가 참이 될 때까지 ψ가 참이어야 한다. φ가 절대 참이 되지 않으면 ψ는 영원히 참으로 유지되어야 한다.
ψ M φ	$\psi\;\mathcal{M}\,\varphi$	Strong release: ψ가 처음으로 참이 되는 시점까지, 그리고 그 시점을 포함하여, φ가 참이어야 하며, 이는 현재 또는 미래의 위치에서 참이어야 한다.

3. 의미론

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

원자 명제 집합의 멱집합 위의 무한 열

: $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

에 대응된다.

ω-단어 ''w''가 LTL 공식 를 만족시킨다는 것은, ''w'' ⊨ 를 의미한다.

로 정의된 ω-언어 ''L''()는 {''w'' | ''w'' ⊨ }이며, 이는 를 만족시키는 ω-단어들의 집합이다.

공식 는 ''만족 가능''하다는 것은, ''w'' ⊨ 를 만족하는 ω-단어 ''w''가 존재한다는 의미이다.

공식 가 ''유효''하다는 것은, 알파벳 2^''AP''에 대한 모든 ω-단어 ''w''에 대해, ''w'' ⊨ 가 성립한다는 의미이다.

추가적인 논리 연산자는 다음과 같이 정의된다.

∧ ≡ ¬(¬ ∨ ¬)
→ ≡ ¬ ∨
↔ ≡ ( → ) ∧ ( → )
'''true''' ≡ ''p'' ∨ ¬''p'', 여기서 ''p'' ∈ ''AP''
'''false''' ≡ ¬'''true'''

추가적인 시간 연산자 '''R''', '''F''', '''G'''는 다음과 같이 정의된다.

'''R''' ≡ ¬(¬ '''U''' ¬) (가 참이 될 때까지 (그리고 그 시점까지) 가 참으로 유지된다. 만약 가 절대로 참이 되지 않으면, 는 영원히 참으로 유지되어야 한다. '''r'''eleases .)
≡ '''true''' '''U''' }} (결국 가 참이 된다)
'''G''' ≡ '''false''' '''R''' ≡ ¬'''F''' ¬ (는 항상 참으로 유지된다)

문자 표기	기호 표기	설명
단항 연산자
N $\phi$	$\circ \phi$	Next: $\phi$ 는 다음 상태에서 참이다. (X로 표기하는 경우도 있다)
G $\phi$	$\Box \phi$	Globally: $\phi$ 는 앞으로 항상 참이다.
F $\phi$	$\Diamond \phi$	Finally: $\phi$ 는 미래의 어느 시점에서 참이 된다.
이항 연산자
$\psi$ U $\phi$	$\psi\mathcal{U}\phi$	Until: $\phi$ 는 현재 또는 미래의 시점에서 참이며, $\psi$ 는 그 시점까지 참이다. 그 시점 이후 $\psi$ 는 참이 될 필요는 없다.
$\psi$ R $\phi$	$\psi\mathcal{R}\phi$	Release: $\psi$ 가 참이 되는 시점까지 $\phi$ 는 참인 상태를 유지한다 (그 후에는 참이 될 필요는 없다). 또한, $\psi$ 가 참이 되지 않는 경우에는, $\phi$ 는 참인 상태를 유지한다.

다음의 항등식이 성립하므로, 연산자의 종류를 줄일 수 있다:

'''F''' $\phi$ = '''true''' '''U''' $\phi$
'''G''' $\phi$ = '''false''' '''R''' $\phi$ = $\neg$ '''F''' $\neg$ $\phi$
$\psi$ '''R''' $\phi$ = $\neg$ ( $\neg$ $\psi$ '''U''' $\neg$ $\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)는 기본 연산자를 통해 정의된 의미와 동치이다.

문자 표기	기호 표기	설명
단항 연산자
N $\phi$	$\circ \phi$	Next: $\phi$ 는 다음 상태에서 참이다. (X로 표기하는 경우도 있다)
G $\phi$	$\Box \phi$	Globally: $\phi$ 는 앞으로 항상 참이다.
F $\phi$	$\Diamond \phi$	Finally: $\phi$ 는 미래의 어느 시점에서 참이 된다.
이항 연산자
$\psi$ U $\phi$	$\psi\mathcal{U}\phi$	Until: $\phi$ 는 현재 또는 미래의 시점에서 참이며, $\psi$ 는 그 시점까지 참이다. 그 시점 이후 $\psi$ 는 참이 될 필요는 없다.
$\psi$ R $\phi$	$\psi\mathcal{R}\phi$	Release: $\psi$ 가 참이 되는 시점까지 $\phi$ 는 참인 상태를 유지한다 (그 후에는 참이 될 필요는 없다). 또한, $\psi$ 가 참이 되지 않는 경우에는, $\phi$ 는 참인 상태를 유지한다.

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 (φ ∨ ψ) ≡ (X φ) ∨ (X ψ)	X (φ ∧ ψ) ≡ (X φ) ∧ (X ψ)	X (φ U ψ)≡ (X φ) U (X ψ)
F (φ ∨ ψ) ≡ (F φ) ∨ ((F ψ)	G (φ ∧ ψ) ≡ (G φ) ∧ ((G ψ)
ρ U (φ ∨ ψ) ≡ (ρ U φ) ∨ (ρ U ψ)	(φ ∧ ψ) U ρ ≡ (φ U ρ) ∧ (ψ U ρ)

부정 전파
'X'는 자기 쌍대	'F와 G'는 쌍대	'U와 R'은 쌍대	'W와 M'은 쌍대
¬X φ ≡ X ¬φ	¬F φ ≡ G ¬φ	¬ (φ U ψ) ≡ (¬φ R ¬ψ)	¬ (φ W ψ) ≡ (¬φ M ¬ψ)
	¬G φ ≡ F ¬φ	¬ (φ R ψ) ≡ (¬φ U ¬ψ)	¬ (φ M ψ) ≡ (¬φ W ¬ψ)

특수한 시간적 속성
F φ ≡ F F φ	G φ ≡ G G φ	φ U ψ ≡ φ U (φ U ψ)
φ U ψ ≡ ψ ∨ ( φ ∧ X(φ U ψ) )	φ W ψ ≡ ψ ∨ ( φ ∧ X(φ W ψ) )	φ R ψ ≡ ψ ∧ (φ ∨ X(φ R ψ) )
G φ ≡ φ ∧ X(G φ)	F φ ≡ φ ∨ X(F φ)

모든 선형 시제 논리 수식은 부정 정규 형식으로 변환할 수 있다. 부정 정규 형식에서는 모든 부정 기호(¬)가 원자 명제 앞에만 나타나고, 다른 논리 연산자 '''참''', '''거짓''', ∧, ∨ 만 나타날 수 있으며, 시간 연산자 '''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 (φ ∨ ψ) ≡ (X φ) ∨ (X ψ)	X (φ ∧ ψ) ≡ (X φ) ∧ (X ψ)	X (φ U ψ)≡ (X φ) U (X ψ)
F (φ ∨ ψ) ≡ (F φ) ∨ ((F ψ)	G (φ ∧ ψ) ≡ (G φ) ∧ ((G ψ)
ρ U (φ ∨ ψ) ≡ (ρ U φ) ∨ (ρ U ψ)	(φ ∧ ψ) U ρ ≡ (φ U ρ) ∧ (ψ U ρ)

부정 전파
'X'는 자기 쌍대	'F와 G'는 쌍대	'U와 R'은 쌍대	'W와 M'은 쌍대
¬X φ ≡ X ¬φ	¬F φ ≡ G ¬φ	¬ (φ U ψ) ≡ (¬φ R ¬ψ)	¬ (φ W ψ) ≡ (¬φ M ¬ψ)
	¬G φ ≡ F ¬φ	¬ (φ R ψ) ≡ (¬φ U ¬ψ)	¬ (φ M ψ) ≡ (¬φ W ¬ψ)

특수한 시간적 속성
F φ ≡ F F φ	G φ ≡ G G φ	φ U ψ ≡ φ U (φ U ψ)
φ U ψ ≡ ψ ∨ ( φ ∧ X(φ U ψ) )	φ W ψ ≡ ψ ∨ ( φ ∧ X(φ W ψ) )	φ R ψ ≡ ψ ∧ (φ ∨ X(φ R ψ) )
G φ ≡ φ ∧ X(G φ)	F φ ≡ φ ∨ X(F φ)

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

5. 다른 논리와의 관계

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

6. 계산 복잡도

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

7. 응용

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

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

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

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

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

7. 1. 모델 검사

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

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

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

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

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

7. 2. 형식 검증

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

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

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

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

7. 3. 기타 응용

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

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

참조

_[1] 서적 "Logic in Computer Science: Modelling and Reasoning about Systems" https://books.google[...]
_[2] 웹사이트 Linear-time Temporal Logic https://web.archive.[...] 2012-03-19
_[3] 서적 Many-dimensional modal logics: theory and applications https://books.google[...] Elsevier
_[4] 웹사이트 First-order Definable Languages http://www.lsv.fr/~g[...]
_[5] 학위논문 Tense Logic and the Theory of Linear Order University of California Los Angeles 1968
_[6] 논문 The temporal logic of programs
_[7] 웹사이트 Principles of Model Checking https://web.archive.[...] MIT Press 2011-05-17
_[8] 문서 Sec. 5.1.5 "Weak Until, Release, and Positive Normal Form" of Principles of Model Checking.
_[9] 서적 Automata, Languages and Programming: 37th International Colloquium, ICALP ... - Google Books https://books.google[...] 2010-06-30
_[10] 서적 25 years of model checking: history, achievements, perspectives http://www.cs.rice.e[...] Springer
_[11] 논문 "On the synthesis of a reactive module" https://doi.org/10.1[...] Association for Computing Machinery, New York, NY, USA
_[12] 논문 An Automata-Theoretic Approach to Linear Temporal Logic. Springer-Verlag
_[13] 논문 Defining Liveness https://doi.org/10.1[...]
_[14] 간행물 Parametric LTL on Markov Chains Springer Berlin Heidelberg 2014
_[15] 서적 Many-dimensional modal logics: theory and applications https://books.google[...] Elsevier

본 사이트는 AI가 위키백과와 뉴스 기사,정부 간행물,학술 논문등을 바탕으로 정보를 가공하여 제공하는 백과사전형 서비스입니다.
모든 문서는 AI에 의해 자동 생성되며, CC BY-SA 4.0 라이선스에 따라 이용할 수 있습니다.
하지만, 위키백과나 뉴스 기사 자체에 오류, 부정확한 정보, 또는 가짜 뉴스가 포함될 수 있으며, AI는 이러한 내용을 완벽하게 걸러내지 못할 수 있습니다.
따라서 제공되는 정보에 일부 오류나 편향이 있을 수 있으므로, 중요한 정보는 반드시 다른 출처를 통해 교차 검증하시기 바랍니다.

문의하기 : help@durumis.com