DL-PA and DCL-PC: model checking and satisfiability problem are indeed in PSPACE

TL;DR

This paper proves that the model checking and satisfiability problems for DL-PA and DCL-PC are in PSPACE, correcting previous misconceptions about their computational complexity.

Contribution

It establishes the PSPACE complexity of these problems and clarifies errors in earlier proofs claiming higher complexity classes.

Findings

Model checking and satisfiability for DL-PA and DCL-PC are in PSPACE.

Previous proofs of EXPTIME-hardness and PSPACE membership were incorrect.

The paper provides corrected complexity classifications for these logics.

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.