논리학에서 선형 시제 논리(線型時制論理, 영어: linear temporal logic, 약자 LTL)는 선형 이산 시간에 대한 여러 가지 양상을 갖춘, 시제 논리의 하나이다. PTL(Propositional temporal logic)이라고도 한다.[1]
통사론[편집]
선형 시제 논리의 논리식은 원자 명제의 유한 집합 및 다음과 같은 논리 연산 기호들로부터 재귀적으로 정의된다.
이들 기호는 다음과 같은 우선순위를 가진다.
- (일항 연산) , , ,
- (명제 논리 밖의 이항 연산) , ,
- (명제 논리의 이항 연산) , ,
이들 기호는 로부터 다음과 같이 유도된다.
이들 기호는 다음과 같이 해석된다.
- : 바로 다음 번에 가 참이다.
- : 결국/언젠가 가 참이다.
- : 항상/언제나 가 참이다.
- : 언젠가부터 영원히 가 참이다.
- : 무한 개의 시점에서 가 참이다.
- : 언젠가 가 참이기 바로 전까지 줄곧 가 참이다.
- : 가 참이기 바로 전까지 줄곧 가 참이다.
- : 가 참일 때까지 줄곧 가 참이다.
의미론[편집]
원자 명제 집합의 멱집합 위의 무한 열
및 선형 시제 논리식 가 주어졌다고 하자. 또한,
와 같이 쓰자. 그렇다면, 가 를 만족시킨다는 것은 와 같이 표기하며, 다음과 같이 재귀적으로 정의된다.
(물론, (), , , , 의 정의로부터 나머지 정의들을 유도할 수 있다.) 이에 따라, 선형 시제 논리식 는 의미론적으로 집합
에 대응된다.
선형 시제 논리식에 대하여, 다음과 같은 논리적 동치·함의 관계가 성립한다.
- 쌍대 법칙
- 멱등 법칙
- 흡수 법칙
- 분배 법칙
-
-
- 전개 법칙
- 기타 법칙
참고 문헌[편집]
- Baier, Christel; Katoen, Joost-Pieter (2008). 《Principles of Model Checking》 (영어). The MIT Press. ISBN 978-0-262-02649-9.