Kernekoncepter
과거 연산자를 포함하는 LTL 공식을 결정적 Rabin 오토마타로 직접 변환하는 방법을 제시한다. 이 변환은 중간 비결정적 오토마타를 거치지 않고 비대칭적으로 최적화된 결과를 산출한다.
Resumé
이 논문은 과거 선형 시간 논리(pLTL)에서 결정적 Rabin 오토마타로의 직접 변환 방법을 제시한다. 이 변환은 중간 비결정적 오토마타를 거치지 않고 비대칭적으로 최적화된 결과를 산출한다.
주요 내용은 다음과 같다:
- pLTL 공식의 과거 정보를 공식 자체에 인코딩하여 백트래킹 없이 미래에서 평가할 수 있도록 한다.
- 'Master Theorem'을 pLTL로 일반화하여 공식의 언어를 단순한 언어들의 부울 조합으로 분해할 수 있다.
- 분해된 언어들에 대해 간단한 인수 조건을 가진 결정적 오토마타를 쉽게 구축할 수 있다.
- 이를 통해 공식 크기의 이중 지수 크기의 결정적 Rabin 오토마타를 구축할 수 있다.
Statistik
공식 크기 n + m에 대해 2^O(n+m) 상태와 최대 2^n 개의 Rabin 쌍을 가지는 결정적 Rabin 오토마타를 구축할 수 있다.
Citater
"과거 연산자의 추가는 초기 동등성에 대한 논리의 표현력을 높이지만, 만족 가능성/타당성 및 모델 검사의 복잡도는 PSPACE-완전 상태로 유지된다."
"특정 속성은 과거 연산자를 사용하여 더 자연스럽고 간결하게 표현할 수 있다."
"과거 연산자를 포함하는 공식 중에는 모든 (초기적으로) 동등한 LTL 공식보다 지수적으로 큰 공식이 존재한다."