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

• Type: Journal
• Year: 2006
• Where: JAPLL
• Authors: Martin Lange
• Keywords: Checking, JAPLL 2006, Model, Propositional Dynamic Logic