Decision procedures for propositional dynamic logics have been
investigated since the introduction of this logic in the late seventies.
Only in recent years have practical procedures been suggested and
implemented. In this talk I will give a general overview of dynamic
logic itself and describe key aspects of decision procedures for the
satisfiability problem in dynamic logic. The focus of the talk will
be on approaches to the construction of benchmarking formulae for the
evaluation of implemented decision procedures. The benchmarking approach
presented in the talk is not specific to dynamic logics, but is intended
to be a general methodology for the evaluation of solvers for
non-classical logics. As a case study I will then present results of such
an evaluation for the current generation of implemented decision procedures
for propositional dynamic logic, namely, the Tableau Workbench by Abate,
Gore, and Widmann (2009), the pdlProver system by Gore and Widmann (2009),
and the MLSolver system by Friedmann and Lange (2009).