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

Philippe Balbiani, Andreas Herzig, François Schwarzentruber, Nicolas Troquard

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.

Knowledge Graph

arrow_drop_up

Comments

Sign up or login to leave a comment