선형 시제 논리

위키백과, 우리 모두의 백과사전.

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

통사론[편집]

선형 시제 논리의 논리식은 원자 명제의 유한 집합 및 다음과 같은 논리 연산 기호들로부터 재귀적으로 정의된다.

이들 기호는 다음과 같은 우선순위를 가진다.

  • (일항 연산) , , ,
  • (명제 논리 밖의 이항 연산) , ,
  • (명제 논리의 이항 연산) , ,

이들 기호는 로부터 다음과 같이 유도된다.

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

  • : 바로 다음 번에 가 참이다.
  • : 결국/언젠가 가 참이다.
  • : 항상/언제나 가 참이다.
  • : 언젠가부터 영원히 가 참이다.
  • : 무한 개의 시점에서 가 참이다.
  • : 언젠가 가 참이기 바로 전까지 줄곧 가 참이다.
  • : 가 참이기 바로 전까지 줄곧 가 참이다.
  • : 가 참일 때까지 줄곧 가 참이다.

의미론[편집]

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

및 선형 시제 논리식 가 주어졌다고 하자. 또한,

와 같이 쓰자. 그렇다면, 를 만족시킨다는 것은 와 같이 표기하며, 다음과 같이 재귀적으로 정의된다.

(물론, (), , , , 의 정의로부터 나머지 정의들을 유도할 수 있다.) 이에 따라, 선형 시제 논리식 는 의미론적으로 집합

에 대응된다.

성질[편집]

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

  • 쌍대 법칙
  • 멱등 법칙
  • 흡수 법칙
  • 분배 법칙
  • 전개 법칙
  • 기타 법칙

각주[편집]

  1. Dov M. Gabbay; A. Kurucz; F. Wolter; M. Zakharyaschev (2003). 《Many-dimensional modal logics: theory and applications》. Elsevier. 46쪽. ISBN 978-0-444-50826-3. 

참고 문헌[편집]

  • Baier, Christel; Katoen, Joost-Pieter (2008). 《Principles of Model Checking》 (영어). The MIT Press. ISBN 978-0-262-02649-9.