PV3 Premise: Predictive Monitoring with Imprecise Sensorscomputes the probability of a user-specified risk in a Markov decision process

Application domain/field

Expected input


Expected output


Premise is built on top of Storm. Uses Z3. By default Premise will simulate 50 traces of 500 steps each. It is possible to simulate more/less traces of a different length by passing additional options when calling Premise.


License: GPL v3.0
Monitoring Probabilistic


Related papers

Runtime Monitors for Markov Decision Processes (CAV '21)

Last publication date

15 July 2021

ProVerB specific

ProVerB is a part of SLEBoK. Last updated: February 2023.