EXPTIME-hardness of higher-dimensional Minkowski spacetime

TL;DR

This paper establishes that the validity problem for basic temporal logic on higher-dimensional Minkowski spacetime is EXPTIME-hard, demonstrating significant computational complexity in this geometric logic setting.

Contribution

It proves EXPTIME-hardness of the validity problem for temporal logic on multi-dimensional Minkowski spacetime, extending complexity results to higher dimensions and different accessibility relations.

Findings

Validity problem is EXPTIME-hard for Minkowski spacetime with multiple dimensions.

Hardness holds for both lightspeed-or-slower and slower-than-light relations.

Reduction from two-player corridor-tiling game demonstrates the complexity.

Abstract

We prove the EXPTIME-hardness of the validity problem for the basic temporal logic on Minkowski spacetime with more than one space dimension. We prove this result for both the lightspeed-or-slower and the slower-than-light accessibility relations (and for both the irreflexive and the reflexive versions of these relations). As an auxiliary result, we prove the EXPTIME-hardness of validity on any frame for which there exists an embedding of the infinite complete binary tree satisfying certain conditions. The proof is by a reduction from the two-player corridor-tiling game.