선형 시간 논리학

논리학에서 선형 시간 논리 또는 선형 시간 시간 논리^[1][2](LTL)는 시간을 가리키는 모달 시간 논리학이다.LTL에서는 어떤 조건이 결국 참이 되고, 다른 사실이 진실이 될 때까지 조건이 참이 되는 등의 경로의 미래에 대한 공식을 암호화할 수 있다.보다 복잡한 CTL*의 단편으로서 분기 시간과 정량자를 추가로 허용한다.그 후 LTL을 명제적 시간 논리, 약칭 PTL이라고 부르기도 한다.^[3]표현력 측면에서 선형 시간 논리(LTL)는 1차 논리학의 단편이다.^[4][5]

LTL은 1977년 Amir Pnueli에 의해 컴퓨터 프로그램의 공식적인 검증을 위해 처음 제안되었다.^[6]

구문

LTL은 유한한 명제 변수 AP, 논리 연산자 ¬과 ∨, 시간적 모달 연산자 X(일부 문헌은 O 또는 N을 사용한다)와 U. 형식적으로 AP에 대한 LTL 공식의 집합은 다음과 같이 귀납적으로 정의된다.

• p ∈ AP인 경우 p는 LTL 공식이다.
• ψ과 φ이 LTL 공식이라면, ,, ,, X and, u U ψ은 LTL 공식이다.^[7]

X는 다음으로 읽히고 U는 그 때까지 읽는다.이러한 기본 연산자 외에 LTL 공식을 간결하게 쓰기 위한 기본 연산자의 관점에서 정의된 논리적, 시간적 연산자가 추가로 존재한다.추가적인 논리 연산자는 ∧, → ↔, ↔, true, false이다.추가 시간 연산자는 다음과 같다.

• G for always (광택)
• 마지막으로 F
• 출시 R
• W: 약자: ~까지
• 강력한 릴리즈를 위한 M

의미론

LTL 공식은 AP에서 변수의 무한 진실 평가 순서에 의해 충족될 수 있다.이러한 시퀀스는 Kripke 구조의 경로에 있는^AP 단어로 볼 수 있다(문자 2에 대한 Ω 단어).w = a₀,a₁,a₂...는 정말 Ω 단어다.Let w(i) = a_i. Let wⁱ = a_i,a_i+1, ...의 접미사 w의 접미사.형식적으로 단어와 LTL 공식 사이의 만족 관계 ⊨은 다음과 같이 정의된다.

• w if p인 경우 p p w(0)
• W ⊨ ¬ψ만약 그렇다면ψ
• w ⊨φ∨ψ만약 그렇다면φ또는 w ⊨ψ
• w ⊨ ψ만약¹ 그렇다면ψ(다음 시간 단계에서)ψ참이어야 함)
• w ⊨φ U ψiⁱ if 0이 존재한다면 w ⊨ψ그리고 모든 0 < k < i^k, w ⊨에 대하여φ(φ때까지 진실성을 유지해야 한다.ψ(진실화)

우리는 Ω-w가 LTL 공식을 만족한다고 말한다.ψw가 있을 때ψ . Ω-언어L()ψ)에 의해 정의됨ψ {ww ⊨}ψ}}을(를) 만족시키는 Ω-words 집합이다.ψ. 공식ψw와 같은 Ω 단어가 존재한다면 만족스럽다.ψ. 공식ψ알파벳 2^AP, w ⊨ 이상의 각 Ω 단어에 대해 유효하다.ψ.

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

• φ∧ψ≡ ¬(¬φ∨ ¬ψ)
• φ→ψ≡ ¬φ∨ψ
• φ↔ψ≡ (φ→ψ) ∧ (ψ→φ)
• 참 p p p p p, 여기서 p ∈ AP.
• 거짓 ≡ ¬진실

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

• ψ R φ≡ ¬(¬ψ U ¬φ) (φ한 번을 포함하기 전까지는 진실이다.ψ사실이 되다만약ψ결코 진실이 되지 않는다.φ영원히 진실로 남아야 한다.)
• F ψ ≡ 참U ψ(eventually)ψ(진실화)
• G ψ ≡ falseR ψ≡ ¬F ¬ψ(ψ항상 진실로 남아 있음)

약해진 후 강력한 해제

일부 저자는 또한 W로 표시된 이진 연산자까지의 약점을 정의하고 있으며, 이때 바이너리 연산자와 유사하지만 정지 조건이 발생할 필요는 없다(해제와 유사).^[8]U와 R 둘 다 다음과 같은 약자의 관점에서 정의될 수 있기 때문에 때때로 유용하다.

• ψ W φ ( ( U φ) ) G ≡ ≡ U ( g G )) ≡ R ( r r ))
• ψ U φ Fφ ( ( w W ))
• ψ R φ ≡ W (φ φ ψ)

M으로 표시된 강력한 방출 이진 연산자는 약자의 이중이다.해제 조건은 어느 시점에서 유지되어야 하기 때문에, 이 값은 ~ 연산자와 유사하게 정의된다.따라서, 그것은 방출 사업자보다 강하다.

• ψ M φ ≡ ((ψ w W ≡) ψ F ψ ≡ r r r r r u u u u u u u u u u u.

시간 연산자에 대한 의미론은 다음과 같이 그림으로 제시한다.

텍스트	상징적	설명	도표
단일 연산자:
X φ	$\displaystyle \bigcircle \varphi }$	neXt: φ은 다음 상태로 유지되어야 한다.
F φ	${\displaystyle \Diamond \varphi }$	마지막으로: φ은 결국 (후행 경로의 어느 곳에서는) 버텨야 한다.
G φ	${\displaystyle \Box \varphi }$	글로벌: φ은 이후의 전체 경로를 고수해야 한다.
이항 연산자:
ψ U φ	${\displaystyle \psi \;{\mathcal {U}\,\varphi }$	~: ψ은 최소한 φ이 참이 될 때까지 버텨야 하며, which은 현재 또는 미래의 위치에서 버텨야 한다.
ψ R φ	${\displaystyle \psi \;{\mathcal {R}\,\varphi }$	해제: φ은 ψ이 처음 진실이 될 때까지 진실해야 하며, ψ이 결코 진실이 되지 않는다면 φ은 영원히 참으로 남아 있어야 한다.
ψ W φ	${\displaystyle \psi \;{\mathcal {W}\,\varphi }$	때까지 약함: ψ은 최소한 φ까지 참아야 하며, φ이 결코 진실이 되지 않으면 ψ은 영원히 참으로 남아 있어야 한다.
ψ M φ	${\displaystyle \psi \;{\mathcal {M}\,\varphi }$	강한 해제: φ은 ψ이 처음으로 참이 되는 지점까지 참이어야 하며, 이 지점은 현재 또는 미래의 위치에서 유지되어야 한다.

등가성

φ, ψ, ρ을 LTL 공식으로 한다.다음 표에는 일반적인 논리 연산자 간에 표준 등가치를 확장하는 유용한 등가성 중 일부가 열거되어 있다.

분배성
X (φ ∨ ψ) ≡ (X φ) ∨ (X ψ)	X (φ ∧ ψ)≡ (X φ)≡ (X φ)	X (φ U ψ)≡ (X φ) U (X ψ)
F (φ) ) (F ≡) f (F ∨) ψ (F ψ)	G (φ ∧ ψ)≡ (G φ) ( (G ))
ρ U (φ ∨ )) ( ( ( ( () ( ( ( ( ()	(φ) U ρ (ρ U ρ) ) (φ ψ) ( () (ψ u)

부정 전파
X는 스스로 이중화한다.	F와 G는 이중이다.	U와 R은 이중이다.	W와 M은 이중이다.
¬X φ X φφ	¬F φ G φ φ	¬ (φ U ψ) ≡ (¬ r r)	¬ (φ W ψ) ≡ (¬φ M ¬ψ)
	¬G φ F φ	¬ (φ R ψ) ≡ (¬φ U ¬ψ)	¬ (φ M ψ) ≡ (¬φ W ¬ψ)

특수 시간 특성
F φ F F φ	G φ G G φ	φ U ≡ ≡ U ( u U ψ)
φ U ψ ≡ ( ( ( ( X (φ U ψ) )	φ W ≡ ψ ( ( ( ( X (ψ W ψ) )	φ R ψ ≡ ψ ( ( X ( x R ψ) )
G φ ≡ φ X(G φ)	F φ ≡ φ X(F φ)

부정 정규 형식

LTL의 모든 공식은 부정 정규 형태로 변환될 수 있다.

• 모든 부정은 오직 원자 명제 앞에만 나타난다.
• 다른 논리 연산자만이 참, 거짓, ∧, ∨만이 나타날 수 있으며,
• 시간 연산자 X, U, R만이 나타날 수 있다.

부정 전파에 대해 위의 동등성을 이용하면 정상적인 형태를 도출할 수 있다.이 정상적인 형태는 LTL의 기본 연산자가 아닌 R, true, false, ∧을 공식에 나타낼 수 있게 한다.부정 정규 형식으로의 변환은 공식의 크기를 증가시키지 않는다는 점에 유의하십시오.이 정상적인 형태는 LTL에서 Büchi 자동화로 번역할 때 유용하다.

다른 로직과의 관계

LTL은 단일 순서 논리인 FO[<](Kamp의 정리라고 알려진 결과)^[9] 또는 동등하게 항성이 없는 언어와 동등한 것으로 보일 수 있다.^[10]

계산 트리 논리(CTL)와 선형 시간 논리(LTL)는 둘 다 CTL*의 하위 집합이지만 비교할 수 없다.예를 들어,

• CTL의 어떤 공식도 LTL 공식 F(G p)에 의해 정의된 언어를 정의할 수 없다.
• LTL의 어떤 공식도 CTL 공식 AG(p → (EXQ ∧ EX¬q) ) 또는 AG(EF(p)로 정의되는 언어를 정의할 수 없다.

그러나 CTL*의 하위 집합은 CTL과 LTL의 적절한 상위 집합이다.

계산 문제

LTL 공식에 대한 모델 검사 및 만족도는 PSPACE-완전한 문제들이다.LTL 합성과 LTL 승리 조건과의 게임 검증 문제는 2EXPTIME-완전이다.^[11]

적용들

자동이식 선형 시간 논리 모델 검사

모델 체크를 하는 중요한 방법은 LTL 연산자를 사용하여 원하는 속성(예: 위에서 설명한 속성)을 표현하고 모델이 이 속성을 충족하는지 실제로 확인하는 것이다.한 가지 기법은 모델과 동등한 부치 오토매틱(모델이라면 정확히 Ω 워드를 받아들인다)과 재산의 부정(정확히 부정된 속성을 만족시키는 Ω 워드를 받아들인다)과 동등한 부치 오토매틱(cf)을 얻는 것이다.Büchi 자동화에 대한 선형 시간 논리).비결정론적 Büchi automata 두 개의 교차점은 모델이 속성을 만족하는 경우에만 비어 있다.^[12]

형식 확인에서 중요한 속성 표현

선형 시간 논리를 사용하여 표현할 수 있는 두 가지 주요 특성이 있는데, 안전 속성은 대개 나쁜 일은 일어나지 않는다고 진술하는 반면(GFψ 또는 G(G) →Fψ)는 좋은 일이 계속 일어난다고 진술하는 것이다.^[13]보다 일반적으로 안전 속성은 모든 counterexample이 한정된 접두사를 갖는 것으로, 무한 경로로 확장되지만, 여전히 counterexample이다.반면, livity 속성의 경우, counterrexample의 모든 유한한 접두사는 공식을 만족하는 무한 경로로 확장될 수 있다.

사양 언어

선형 시간 논리학의 적용 중 하나는 선호 기반 계획을 위한 계획 도메인 정의 언어의 선호 사양이 된다.^{[citation needed]}

확장

파라메트릭 선형 시간 논리는 LTL을 by-modality에 대한 변수로 확장한다.^[14]

참고 항목

위키미디어 커먼즈에는 선형 시간 논리 관련 미디어가 있다.

• 액션어
• 미터법 시간 논리

참조

외부 링크

• LTL 발표회
• 선형시점논리와 부치오토마타
• Bozen-Bolzano 자유대학의 알레산드로 아르탈레 교수의 LTL 티칭 슬라이드
• LTL에서 Buchi 번역 알고리즘까지, 모델 확인을 위한 Spot의 웹사이트에서 계보.