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

Application domain/field

• Monitoring
• Cyber-physical systems
• Markov decision process (MDP)
• Probabilistic model checking
• Runtime verification
• Runtime monitoring

Expected input

• Markov Devision Process (MDP)
• State risk, e.g. the probability that the plane will crash into a vehicle within a given number of steps.

Format:

• Markov Decision Process: .nm file, extended dialect of the PRISM language
• State risk: PCTL (probabilistic CTL) formula, passed as an argument when calling Premise

Expected output

• File with some model-related statistics
• .csv file for each trace, containing the calculated risk for that trace.

Internals

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.

Comments

License: GPL v3.0