A prototype using ltl2ldba
(Owl) for quantitative model checking of MDPs (Markov decision process). Based on the PRISM model checker.
The development repositories are not public at the moment. But a recent snapshot of the source code and a pre-built version (with startup script) can be obtained here:
MoChiBA
only requires an installed Java 8 Runtime Environment.
The tool cannot be configured - all optimisations are enabled - and does not need to be installed.
It reads a model (given as an MDP, .nm
) and a property specification (.pctl
) from the file system and prints the results to stdout
.
java -jar mochiba.jar model.nm properties.pctl
We performed benchmarks on two case studies and publish here the models, specifications and the raw log output:
Since in most default configuration the Java JRE is too conservative with the heap and stack size, we recommend using the included sh
script to start the tool, which fine tunes the JRE for MoChiBA
.
./mochiba.sh model.nm properties.pctl
MoChiBA is short for Quantitative Probabilistic LTL Model Checking using Limit-Deterministic Büchi Automata.
It is a well-known fact that naming things is a hard problem. After spending some time searching for a good name we only came up with candidates too close1 to already used names (e.g. ProB, PRISM) or unpronounceable ones such as QuPrLimBü or ProLimDeBüchi. So after some toying around we discovered one could form the word mochi (a delicious Japanese rice cake) from Model Checking and adding BA for Büchi automaton yielded something pronounceable. We also noticed that it contains Chiba, the name of the city where ATVA 2016 will take place (the whole word has also another meaning in Japanese: Translations) and at this point we didn’t want to further tempt fate for a project that is submitted to ATVA 2016. :)
1: Edit distance less than 2.
Salomon Sickert, Jan Křetínský
MoChiBA: Probabilistic LTL Model Checking using limit-deterministic Büchi Automata
ATVA (2016): bibtex / view / full version
Salomon Sickert, Javier Esparza, Stefan Jaax, Jan Křetínský
Limit-Deterministic Büchi Automata for Linear Temporal Logic
CAV (2016): bibtex / view / full version