NEXP-completeness and Universal Hardness Results for Justification Logic

TL;DR

This paper establishes tight NEXP-completeness bounds and universal hardness results for multi-agent justification logic satisfiability problems, advancing understanding of their computational complexity.

Contribution

It provides the first tight NEXP bounds and broad hardness results for multi-agent justification logics, improving previous single-agent bounds and answering open questions.

Findings

Satisfiability for multi-agent justification logic is NEXP-complete.

Satisfiability is Sigma 2 p-hard under certain conditions.

Results extend previous bounds from single-agent to multi-agent cases.

Abstract

We provide a lower complexity bound for the satisfiability problem of a multi-agent justification logic, establishing that the general NEXP upper bound from our previous work is tight. We then use a simple modification of the corresponding reduction to prove that satisfiability for all multi-agent justification logics from there is hard for the Sigma 2 p class of the second level of the polynomial hierarchy - given certain reasonable conditions. Our methods improve on these required conditions for the same lower bound for the single-agent justification logics, proven by Buss and Kuznets in 2009, thus answering one of their open questions.