Description

This project targets at developing an editor for spacial models which can be used for performance evaluation of new model checking methods. As an example, consider the example at https://core.ac.uk/download/pdf/80780059.pdf, Section 2. Here, a new model checking method is evaluated using scenarios where we have two robots operating in a grid world with antagonistic behaviours. Using the editor developed in this project, it shall be possible to develop similar spacial models. It shall be possible to load models, store models, and to export them to either the language of the probabilistic model checker PRISM (http://www.prismmodelchecker.org/) or in JANI (https://pure.qub.ac.uk/portal/files/161670364/paper.pdf).
Other details: This is a project of medium difficulty. The implementation language is the choice of the student. It would be useful if the student knew about modelling languages, but this is not a strict requirement.