DL-PA and DCL-PC: model checking and satisfiability problem are indeed in PSPACE
Logic in Computer Science
2014-12-01 v1
Abstract
We prove that the model checking and the satisfiability problem of both Dynamic Logic of Propositional Assignments DL-PA and Coalition Logic of Propositional Control and Delegation DCL-PC are in PSPACE. We explain why the proof of EXPTIME-hardness of the model checking problem of DL-PA presented in (Balbiani, Herzig, Troquard, 2013) is false. We also explain why the proof of membership in PSPACE of the model checking problem of DCL-PC given in (van der Hoek, Walther, Wooldridge, 2010) is wrong.
Cite
@article{arxiv.1411.7825,
title = {DL-PA and DCL-PC: model checking and satisfiability problem are indeed in PSPACE},
author = {Philippe Balbiani and Andreas Herzig and François Schwarzentruber and Nicolas Troquard},
journal= {arXiv preprint arXiv:1411.7825},
year = {2014}
}