  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.
