The Undecidability of Arbitrary Arrow Update Logic
Logic in Computer Science
2016-09-20 v1
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.
Keywords
Cite
@article{arxiv.1609.05686,
title = {The Undecidability of Arbitrary Arrow Update Logic},
author = {Hans van Ditmarsch and Wiebe van der Hoek and Louwe B. Kuijer},
journal= {arXiv preprint arXiv:1609.05686},
year = {2016}
}