PRISM Model Checker

Mentors: Student: Nicolas Del Piano

<p>Nowadays, most floating point computations are performed in double precision – with a mantissa of 53 bits. Nevertheless, depending on the application we are using, it is preferable more precision, such as double extended – 64 bits – quadruple extended – 113 bits – or even more. The main goal of this project is to research how we can achieve such arbitrary precision on PRISM – by this, we mean the user should be able to choose the precision of each calculation – in order to provide a close approximation of exact solutions.</p>

Mentors: Student: Muhammad Omer Saeed

<p>Prism is a tool for probabilistic model checking. It is categorized as a formal verification system tool for the modelling and analysis of systems that exhibit probabilistic behavior. Prism allows its users to plot the results of its various experiments graphically, but currently only a small range of graphs is supported. This proposal addresses the extension of the graphing capabilities of Prism by adding the support of many new 2D and 3D plots. This feature would enable the users of Prism to easily grasp and compare the results of the experiments run on this tool without having to go through the text output results. This project also addresses the enhancement of the general GUI of Prism. This would focus on making this tool more flexible and usable.</p>

Mentors: Student: christopherZ

<p>In this project the multi-objective mean-payoff properties in Markov decision process are to be added into Prism, which is a probabilistic model checker. In this project the following things are done to Prism:</p> <p>• Multi-objective mean-payoff properties support in Markov decision process is extended, namely the algorithm defined in [1] is planned to be added. This should be based on the already existing MultiGain.</p> <p>• A conversion algorithm for f LT L (GU ) formulae to a MOMP, defined in [2].</p> <p>• The (already existing) Rabinizer for converting LTL to DTGRA, be- cause it heavily intersects with the conversion algorithm for f LT L (GU ) .</p> <p>[1] Chatterjee, Krishnendu, Zuzana Komarkova, and Jan Kretinsky. ”Uni- fying two views on multiple mean-payoff objectives in Markov deci- sion processes.” Logic in Computer Science (LICS), 2015 30th Annual ACM/IEEE Symposium on. IEEE, 2015.</p> <p>[2] Forejt, V., J. Krcl, and J. Kretnsk. ”Controller synthesis for MDPS and frequency LTL GU (2015).” CoRR, abs/1509.04116.</p>

Mentors: Student: Ganindu

<p>Prism is a probabilistic model checker, by which, the users can model and analyse real time systems. Prism provides its own modelling language. A user can model a system using this language, see a graphical representation of the model and check the behaviour of the model against the optimal strategy (adversary).</p> <p>The aim of the project is to enhance the support for strategies, which will enable more flexible/complex types of strategies/checks which are currently not supported. It will also allow the users to visualize the behaviour of the optimal adversary in a more user-friendly way, and to modify it and re-check with the model. And it will enhance the support for the features like exporting, importing and re-verification of strategies, which are already available in the tool, but not with full functionality.</p>

Mentors: Student: Maximilian Probst

<p>During the project the current model construction will be analysed in regard to performance(i.e. reachability of multiple initial states, scalability and comprehensiveness(adding support for other types of models, i.e. PTAs). Depending on the analysis, it is decided which changes in the current approach enhance the functionality/ performance/ scalability and together with the supervisor a feature list can be defined. Then the implementation of the features is conducted and additionally efficient transformation to a sparse model and full import/export of the explicit model is implemented.</p>