Core Concepts
이 논문은 양상 논리 InqM과 탐구 명제 논리 InqB의 모델 체크 문제가 PSPACE-완전하다는 것을 보여준다.
Abstract
이 논문은 다음과 같은 내용을 다룹니다:
양상 논리 InqM과 탐구 명제 논리 InqB의 기본 개념을 소개합니다. 이 논리들은 질문을 다룰 수 있는 논리 체계입니다.
InqM과 InqB의 모델 체크 문제 MC(InqM)과 MC(InqB)를 정의하고, 이 문제들이 PSPACE 복잡도 클래스에 속한다는 것을 보여줍니다. 이를 위해 교대 튜링 기계 알고리즘을 제시합니다.
진리값 양화 불리언 공식 문제 TQBF를 MC(InqB)로 다항식 공간 환원하여, MC(InqB)와 MC(InqM)이 PSPACE-완전하다는 것을 증명합니다.
이를 통해 양상 논리와 탐구 명제 논리의 모델 체크 문제가 매우 복잡한 문제라는 것을 보여줍니다.
Stats
진리값 양화 불리언 공식 문제 TQBF는 PSPACE-완전하다.
모델 체크 문제 MC(InqM)과 MC(InqB)는 PSPACE 복잡도 클래스에 속한다.
모델 체크 문제 MC(InqB)는 TQBF 문제에 다항식 공간 환원된다.
Quotes
"The main question we tackle in this paper is: how hard is it to decide if a formula of InqB (resp., InqM) is supported by an information state in a given model?"
"We give a reduction of the PSPACE-complete problem true quantified Boolean formulas TQBF (see, e.g., [7, Ch. 8]) to MC(InqB), thus settling that both MC(InqB) and MC(InqM) are PSPACE-complete."