Introduction

Installing PRISM

• Instructions
• Common Problems And Questions

The PRISM Language

• Introduction
• Example 1
• Model Type
• Modules And Variables
• Commands
• Parallel Composition
• Local Nondeterminism
• CTMCs
• Example 2
• Constants
• Expressions
• Synchronisation
• Module Renaming
• Multiple Initial States
• Global Variables
• Formulas And Labels
• Costs And Rewards
• Real-time Models
• Partially Observable Models
• Uncertain Models
• Process Algebra Operators
• PRISM Model Files

Property Specification

• Introduction
• Identifying A Set Of States
• The P Operator
• The S Operator
• Reward-based Properties
• Multi-objective Properties
• Real-time Models
• Partially Observable Models
• Uncertain Models
• Non-probabilistic Properties
• Syntax And Semantics
• Filters
• Properties Files

Running PRISM

• Starting PRISM
• Loading And Building a Model
• Debugging Models With The Simulator
• Exporting The Model
• Model Checking
• Statistical Model Checking
• Computing Steady-state And Transient Probabilities
• Experiments
• Strategies
• Support For PEPA Models
• Support For SBML
• Explicit Model Import
• Parametric Model Checking

Configuring PRISM

• Introduction
• Computation Engines
• Solution Methods And Options
• Automata Generation
• Other Options

References

Appendices

• Explicit Model Files