pith. sign in

arxiv: 1411.7825 · v1 · pith:HPYO6FMUnew · submitted 2014-11-28 · 💻 cs.LO

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

classification 💻 cs.LO
keywords checkingmodelproblemdcl-pcdl-papspaceexplainlogic
0
0 comments X
read the original 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.

This paper has not been read by Pith yet.

discussion (0)

Sign in with ORCID, Apple, or X to comment. Anyone can read and Pith papers without signing in.