Probabilistic symbolic model checking with PRISM: a hybrid approach

By Marta Z. Kwiatkowska, Gethin Norman, David Parker. International Journal on Software Tools for Technology Transfer (STTT), 2004

527 citations recorded by the source corpus.

Subfields: Computational Theory and Mathematics, Software

View Paper: https://www.semanticscholar.org/paper/5530dd91f145a67d2aec1f78b58aa20c54e06a34

How researchers see this paper

The researchers whose trusted networks rank it highest, strongest advocate first. Every researcher gets a different order.

In Computational Theory and Mathematics

1. Marta Z. Kwiatkowska
2. David Parker
3. Gethin Norman
4. Axel van Lamsweerde
5. Jane Hillston
6. Emmanuel Letier
7. Joost-Pieter Katoen
8. Christel Baier

In Software

1. Axel van Lamsweerde
2. Marta Z. Kwiatkowska
3. David Parker
4. Gethin Norman
5. Jane Hillston
6. Emmanuel Letier
7. Joost-Pieter Katoen
8. Christel Baier

Citations in the corpus

• Principles of model checking (2008, methodology): “– powerful tools: PRISM (4,000 downloads), MRMC, Petri net tools, Probmela – applications: distributed systems, biology, avionics, . . . c© JPK 10 Probability elsewhere • In performance modelling (Erlang, 1907) – models: typically continuous-time Markov chains – emphasis on steady-state and transien”
• Reasoning about partial goal satisfaction for requirements and design engineering (2004, methodology): “Probabilistic model checkers such as PRISM [15] or ETMCC [10] may be used to check whether a given probabilistic transition system satisfies some probabilistic temporal assertion.”
• Stochastic Model Checking (2007, methodology): “More specifically, since we need to store numerical values, PRISM uses multi-terminal binary decision diagrams (MTBDDs) [21,7] and a number of variants [46,52,48] developed to improve the efficiency of probabilistic analysis, which involve combinations of symbolic data structures such as MTBDDs and ”
• A Program Logic for Union Bounds (2016, unknown): “Probabilistic model-checking is a successful line of research that has delivered mature and practical tools and addressed a broad range of case studies; Baier and Katoen [2], Katoen [26], Kwiatkowska et al. [30] cover some of the most interesting developments in the field.”
• Approximate Computing: A Survey (2016, methodology): “The popular tools MRMC [29] and PRISM [31] have been used in diverse fields ranging from analyzing the source code of wireless protocols for faults to modeling human driver behavior for use in autonomous driving systems.”
• Dynamic QoS Management and Optimization in Service-Based Systems (2011, methodology): “To check if a Markov model satisfies its QoS requirements , numerical/symbolic [6], [8], [16], [53] and statistical [100] techniques have been developed, and extensive tool support is available (e.g., PRISM [72]).”
• Approximate Probabilistic Model Checking (2004, background): “PRISM [7,15] is a probabilistic symbolic model checker that can check PCTL formulas on fully or concurrent probabilistic systems.”
• Fluid flow approximation of PEPA models (2005, methodology): “We compare against steady-state and transient analysis as implemented by the PRISM probabilistic model-checker [17], which provides PEPA as one of its input languages.”