Sciweavers

JAPLL
2006

Model checking propositional dynamic logic with all extras

13 years 3 months ago
Model checking propositional dynamic logic with all extras
This paper presents a model checking algorithm for Propositional Dynamic Logic (PDL) with looping, repeat, test, intersection, converse, program complementation as well as context-free programs. The algorithm shows that the model checking problem for PDL remains PTIME-complete in the presence of all these operators, in contrast to the high increase in complexity that they cause for the satisfiability problem. Key words: Propositional Dynamic Logic, Model Checking, Complexity
Martin Lange
Added 13 Dec 2010
Updated 13 Dec 2010
Type Journal
Year 2006
Where JAPLL
Authors Martin Lange
Comments (0)