Tool Documentation for mcpdl


Copyright © 2008 Roland Axelsson

The source code in the provided package may be used under the terms of the BSD license. Please read the file 'COPYING' for details.


The program mcpdl is a model checker for Propositional Dynamic Logic with Indexed Grammars (PDL[IG])). The model and specification has to be provided explicitly via an input file as described in the model specification language (MSL). Note that the implementation has not yet been tested thoroughly yet.


This distribution comes with no warranty whatsoever and is distributed under the BSD license (see above).

Feel free to provide your personal details.



The following tools and libraries have to be installed on your system:

Download the above file mc_pdlig.tgz. Unpack the files. Switch to the top-level directory of the distribution and edit the marked passages in the Makefile. Execute the following commands in the top-level directory:

touch .depend

This should result in an executables mcpdl in the ./bin directory.


mcpdl takes as input a text file with a string content as specified in the MSL documentation page. In its SPEC section a formula in PDL[IG] should be provided over which the model is checked.
There are several options which can be displayed with mcpdl -help:

  • -v <level>
    defines the verbosity level of the execution. <level> may take values between 0 and 3, where 0 is quiet and 3 is extremely verbose.
  • --quiet
    no output other than errors, same as -v 0
  • --msg
    a few basic messages about the program status, same as -v 1
  • --verbose
    detailled information about the model checking progress, same as -v 2
  • --debug
    almost unreadable very low level debug information, same as -v 3
  • -t <secs>
    timeout for the model checking procedure in seconds, causes the program to terminate at the first possible occasion (after finishing the current subformula which in most cases should be almost immediately)
  • --timeout <secs>
    same as -t <secs>
  • -help
    displays a list of options similar to this
  • --help
    same as -help


Depending on the verbosity level in which the tools are executed, there is textual output. Unless sojourning in the highest of these levels, its meaning should be more or less clear, at least if the user has read the papers on which the tool relies. At the end, there is output of a result set containing those states which satisfy the specification formula.

Bug Reports:

I am grateful for every report on existing bugs in the software. Please send to:

to make mail visible: move mouse over

Last modified: Thu Jun 26 17:31:30 2008