Description

Finding good state elimination orders

State elimination is a method which has been used in a wide variety of methods for the analysis of Markov models.

https://dblp.uni-trier.de/rec/conf/atva/GainerHS18.html?view=bibtex
https://dblp.uni-trier.de/rec/conf/qest/GainerHS18.html?view=bibtex
https://dblp.uni-trier.de/rec/conf/setta/HahnH16.html?view=bibtex
https://dblp.uni-trier.de/rec/conf/tase/ChenHHKQ013.html?view=bibtex
https://dblp.uni-trier.de/rec/journals/sttt/HahnHZ11.html?view=bibtex
https://dblp.uni-trier.de/rec/conf/nfm/HahnHZ11.html?view=bibtex
https://dblp.uni-trier.de/rec/conf/cav/HahnHWZ10.html?view=bibtex
https://dblp.uni-trier.de/rec/conf/spin/CalinCDHZ10.html?view=bibtex
https://dblp.uni-trier.de/rec/conf/spin/HahnHZ09.html?view=bibtex

The principle idea of state elimination is as follows: The original stochastic model is transformed by removing all but a few states. This is done in such a way that the value of the property (such as for instance the probability to reach a given set of unsafe states) under consideration is maintained. While state elimination has advantages over other solution methods (such as value iteration), one problem is to find the best sequence of states to eliminate. If states are eliminated in a bad order, the intermediate models produced might get get larger than necessary, which means that the overall process will be slower or that too much memory is required.

The objective of this proposed project is to find good a good order in which states are to be eliminated. The exact content of the project could, within others, consist of

- theoretical reasoning about good elimination orders depending on features of the model,
- writing a tool which allows a user to manually decide on the order of which to eliminate states and then to eliminate them,
- allow the users to specify elimination orders in a scripting language such as Lua or JavaScript.

The default technical setting is such that the tool would be implemented
- in (the already working subset of) C++20,
- using OpenGL/WebGL and the Dear ImGui graphical user interface,
- in a way that both usual C++ compilers can be used to produce a desktop version for Windows, macOS, or Linux,
- as well as Emscripten so as to produce a version of the tool which can run in a browser.
For this setting, the supervisor has already checked the principle feasibility. However, he is also fine if other technical solutions are used, as long as the student is aware that the support might not be as good as for the proposed solution.