The Undecidability of Arbitrary Arrow Update Logic

TL;DR

This paper proves that the satisfiability problem for Arbitrary Arrow Update Logic is undecidable by reducing it to the tiling problem, highlighting fundamental limits in the logic's computational properties.

Contribution

It establishes the undecidability of the satisfiability problem for Arbitrary Arrow Update Logic, a significant open question in the field.

Findings

The satisfiability problem is co-RE hard.

Undecidability is proven via reduction from the tiling problem.

Properties of the logic's decidability status are clarified.

Abstract

Arbitrary Arrow Update Logic is a dynamic modal logic that uses an arbitrary arrow update modality to quantify over all arrow updates. Some properties of this logic have already been established, but until now it remained an open question whether the logic's satisfiability problem is decidable. Here, we show that the satisfiability problem of Arbitrary Arrow Update Logic is co-RE hard, and therefore undecidable, by a reduction of the tiling problem.