A model checking procedure for propositional dynamic logic based on the paper of Lange (2006) built on Python 3.7.2. The program first takes a Kripke structure and then checks whether or not a manually (or automatically) given formula holds.
Run the script 'main.py' with additional arguments specifying if you want to generate a Kripke structure from a txt file, randomly or with a specific form (a line or circle graph; these are to be used for testing the completion time); for Kripke structures with more than 400 states, adding the command '--sparse' at the end is recommended. After all this the user will be prompted to enter a PDL formula. Press 'H' for help with syntax.