Title
DL-PA and DCL-PC: model checking and satisfiability problem are indeed in PSPACE.
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.
Year
Venue
Field
2014
CoRR
Discrete mathematics,Model checking,Boolean satisfiability problem,Algorithm,PSPACE,Dynamic logic (digital electronics),Delegation,Mathematics
DocType
Volume
Citations 
Journal
abs/1411.7825
3
PageRank 
References 
Authors
0.42
5
4
Name
Order
Citations
PageRank
Philippe Balbiani195988.63
Andreas Herzig234837.15
François Schwarzentruber317029.05
Nicolas Troquard426629.54