@INPROCEEDINGS{Hustadt+Schmidt@PAAR2010,
 AUTHOR        = {Hustadt, Ullrich and Schmidt, Renate, A.},
 TITLE         = {A Comparison of Solvers for Propositional Dynamic Logic},
 BOOKTITLE     = {Proceedings of the Workshop on Practical Aspect of Automated Reasoning (PAAR-2010)
 [Edinburgh, Scotland, 14 July 2010]},
 YEAR          = {2010},
 EDITOR        = {Konev, B. and Schmidt, Renate A. and Schulz, Stephan},
 PAGES         = {},
 CADDRESS      = {Edinburgh, Scotland},
 CYEAR         = {2010},
 CMONTH        = jul # {~14},
 URL           = {Hustadt+Schmidt@PAAR2010.pdf},
 ABSTRACT      = {Calculi 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 paper, we compare three such systems, namely, the
Tableau Workbench by Abate, Goré, and Widmann
(2009), the pdlProver system by Goré and Widmann (2009), and
the MLSolver system by Friedmann and Lange (2009).
<p>
The benchmarking formulae used in this paper are available in
MLSolver and pdlProver syntax:
<ul style="margin-top: -10; margin-left: 0; padding-left: 20px;">
<li>C<sub>PDL</sub><sup>1</sup> (n=5, k=3, p=0.5): 
in <a href="http://www.csc.liv.ac.uk/~ullrich/samples/paar2010/mlsolver-Cpdl1-5-3.zip">MLSolver syntax</a>, 
in <a href="http://www.csc.liv.ac.uk/~ullrich/samples/paar2010/pdlProver-Cpdl1-5-3.zip">pdlProver syntax</a>
</li>
<li>C<sub>PDL</sub><sup>2</sup> (n=5, k=3, p=0.5): 
in <a href="http://www.csc.liv.ac.uk/~ullrich/samples/paar2010/mlsolver-Cpdl2-5-3.zip">MLSolver syntax</a>, 
in <a href="http://www.csc.liv.ac.uk/~ullrich/samples/paar2010/pdlProver-Cpdl2-5-3.zip">pdlProver syntax</a>
</li>
</ul>}
}