View - Edit - Print - Search

PRISM Manual   version 3.2

---

Contents

---

Introduction

Installing PRISM

• Instructions
• Common Problems And Questions

The PRISM Language

• Introduction
• Example 1
• Model Type
• Modules And Variables
• Initial States
• Commands
• Parallel Composition
• Local Nondeterminism
• Module Renaming
• Example 2
• Constants
• Expressions
• Synchronisation
• Process Algebra Operators
• Global Variables
• Formulas And Labels
• PRISM Language Files
• Costs And Rewards

Property Specification

• Introduction
• Identifying A Set Of States
• Basic Syntax
• The P Operator
• The S Operator
• Satisfaction Of Properties
• Determining The Actual Probability
• Properties Files
• Specification Of Reward-based Properties

Running PRISM

• Starting PRISM
• Loading And Building a Model
• Debugging Models With The Simulator
• Exporting The Model
• Model Checking
• Approximate Computation Of Quantitative Properties
• Computing Steady-state And Transient Probabilities
• Experiments
• Support For PEPA Models
• Support For SBML
• Explicit Model Import

Configuring PRISM

• Introduction
• Computation Engines
• Iterative Numerical Methods
• Other Options

References

---

Introduction

---

PRISM is a probabilistic model checker, a tool for the modelling and analysis of systems which exhibit probabilistic behaviour. Probabilistic model checking is a formal verification technique. It is based on the construction of a precise mathematical model of a system which is to be analysed. Properties of this system are then expressed formally in temporal logic and automatically analysed against the constructed model.

PRISM supports three types of probabilistic models:

• discrete-time Markov chains (DTMCs),
• Markov decision processes (MDPs),
• continuous-time Markov chains (CTMCs).

Models are supplied to the tool by writing descriptions in the PRISM language, a simple, high-level modelling language.

Properties of these models are written in the PRISM property specification language which is based on the two probabilistic temporal logics

• PCTL (probabilistic computation tree logic) for DTMCs and MDPs,
• CSL (continuous stochastic logic) for CTMCs.

plus a number of custom features and extensions.

PRISM performs automatic analysis of such properties using either formal verification techniques based on numerical computation, or discrete-event simulation.

---

Installing PRISM

---

Instructions

Prerequisites

PRISM is known to run on Linux, Windows, Mac OS X and Solaris, including 64-bit variants of several of these operating systems.

You will need Java, more specifically Sun's distribution of Java. To run binary versions of PRISM, you only need the Java Runtime Environment (JRE), not the full Java Development Kit (JDK). Binaries are currently built using Java 6. If you are compiling from source, version 5.0 (sometimes also called version 1.5) or above is sufficient. If you don't know what version of Java you have, type java -version from a command prompt.

To compile PRISM from source, you need the Java Development Kit (JDK), GNU make and a C/C++ compiler (e.g. gcc/g++). For compilation under Windows, you will need Cygwin. See below for more information.

---

Installation on Windows

To install the latest versions of PRISM on Windows, just run the self-extracting installer which you downloaded. For older versions (3.0 and earlier) you need to unpack the zip file by hand. In either case, you do not need administrator privileges to install PRISM - you just need to have write access to the directory in which you plan to install it.

If requested, the installer will place shortcuts to run PRISM on the desktop and/or start menu. If not, you can run by PRISM double-clicking the file xprism.bat (which may just appear as xprism) in the bin folder of your PRISM folder. If nothing happens, the most likely explanation is that Java is not installed or not in your path. To check, open a command prompt window, navigate to the PRISM directory, type cd bin, then xprism.bat and examine the resulting error.

If you want to create shortcuts to xprism.bat manually, you will find some PRISM icons in the etc folder. It is also best to change the "Run" option in the shortcut properties window from "Normal window" to "Minimized".

If you wish to use the command-line version of PRISM on Windows, open a command prompt window and type for example:

You can also edit the file bin\prism.bat to allow it to be run from any location. See the instructions within the file for further details.

PRISM is also known to run on 64-bit versions of Windows. Since we currently only provide 32-bit binary versions, this will only work if you are also running a 32-bit version of Java. If this is not possible for some reason, you will have to build PRISM from source using Cygwin (See below).

Problems? See the section "Common Problems And Questions''.

---

Installation of (non-Windows) binary versions

To ensure compatibility, we recommend that you compile PRISM from source on non-Windows platforms. See below for instructions. However, we do provide pre-compiled binary distributions for Linux (32-bit) and, depending on availability other operating systems such as Mac OS X and Solaris.

To install a binary distribution, unpack the tarred/zipped PRISM distribution into a suitable location, enter the directory and run the install.sh script, e.g.:

You do not need to be root to install PRISM. The install script simply makes some small customisations to the scripts used to launch PRISM. The PRISM distribution is self-contained and can be freely moved/renamed, however if you do so you will need to re-run ./install.sh afterwards.

To run PRISM, execute either the xprism or prism script (for the graphical user interface or command-line version, respectively). These can be found in the bin directory. These scripts are designed to be run from anywhere and you can easily create symbolic links or aliases to them. If you want icons to create desktop shortcuts to PRISM, you can find some in the etc directory.

Problems? See the section "Common Problems And Questions''.

---

Building PRISM from source

To compile PRISM form source code, you will need:

• GNU make (sometimes called gmake)
• a C/C++ compiler (e.g. gcc/g++)
• Sun's Java Development Kit (JDK), version 5.0 (sometimes called 1.5) or higher

To check what version of Java you have, type java -version. To check that you have the development kit, type javac. If you get an error message that javac cannot be found, you probably do not have the JDK installed (or your path is not set up correctly).

Hopefully, you can build PRISM simply by entering the PRISM directory and running make, e.g.:

For this process to complete correctly, PRISM needs to be able to determine both the operating system you are using and the location of your Java distribution. If there is a problem with either of these, you will see an error message and will need to specify one or both of these manually, such as in these examples:

Note the use of double quotes for the case where the directory contains a space. If you don't know the location of your Java installation, try typing which javac. If the result is e.g. /usr/java/jdk1.5.0/bin/javac then your Java directory is /usr/java/jdk1.5.0. Sometimes javac will be a symbolic link, in which case use "ls -l" to determine the actual location.

It is also possible to to set the environment variables OSTYPE and JAVA_DIR directly or edit their values in the Makefile directly. Note that even when you specify JAVA_DIR explicitly (in either way), PRISM still uses the versions of javac (and javah) that are in your path so make sure this is set up correctly.

PRISM has also been successfully compiled under Linux on a variety of 64-bit architectures. The Makefile will try to detect this but, if this does not work for some reason, you can override detection by setting ARCH to either amd64 (for AMD/Intel 64) or ia64 (for Itanium). For example:

Problems? See the section "Common Problems And Questions''.

---

Building PRISM from source on Windows using Cygwin

The compilation of PRISM currently relies on a Unix-like environment. On Windows, this can be achieved using the Cygwin development environment (or alternatively using MSYS). Once Cygwin is installed, you can proceed as described in the previous section. Note that the PRISM compilation process uses the MinGW libraries so that the final result is independent of Cygwin at run-time.

One thing to note: please unzip the PRISM distribution from within Cygwin (e.g. using tar xfz prism-XXX-src.tar.gz). Don't use a Windows program (Winzip, etc.) since this can cause problems.

Problems? See the section "Common Problems And Questions''.

---

Building PRISM from source on Windows using MSYS

Compiling from source in MSYS is less obvious as this environment is currently not directly supported in the makefile. Additionally, MSYS does not handle symlinks in the same way as cygwin does. The first problem is fixed by providing a OSTYPE variable to the makefile, whereas the second problem currently has to be solved manually.

At some point it will fail, saying that it cannot find the CUDD library, this is due to the failing symlinks. We can solve this by means of a few commands:

Problems? See the section "Common Problems And Questions''.

---

Common Problems And Questions

This section describes some of the most common problems and questions related to the installation and running of PRISM. These are grouped into the following categories:

• Running PRISM on Windows
• Running PRISM on non-Windows platforms
• Compiling PRISM
• Other issues

---

Running PRISM on Windows

When I try to run PRISM on Windows, I double-click the PRISM shortcut but nothing happens.

---

Running PRISM on non-Windows platforms

When I try to run PRISM, I get an error of the form:
Exception in thread "main" java.lang.NoClassDefFoundError: ...

When I try to run PRISM, I get an error of the form:
java.lang.UnsatisfiedLinkError: no prism in java.library.path

When I try to run PRISM, I get an error of the form:
Exception in thread "main" java.lang.UnsupportedClassVersionError: Bad version number in .class file

When I try to run a (Linux) binary version of PRISM, I get an error saying that libstdc++.so.5 cannot be found or libstdc++.so.6 cannot be found.

When I try to run PRISM, I get an error of the form:
Exception in thread "main" java.lang.ExceptionInInitializerError
at java.lang.Class.initializeClass(libgcj.so.7)
at prism.PrismSettings.<init>(PrismSettings.java:297)

When I try to run PRISM, I get an error of the form:
java.lang.UnsatisfiedLinkError: libprism: ... cannot restore segment prot after reloc: Permission denied

Do I have to use Sun's version of Java to build/run PRISM?

---

Compiling PRISM

I can't compile PRISM on Fedora 9. Why not?

When I try to compile PRISM, make seems to get stuck in an infinite loop

When I try to compile PRISM, I get errors of the form:
/usr/bin/libtool: for architecture: cputype (16777234) cpusubtype (0) file: -lSystem is not an object file (not allowed in a library)

When I try to compile PRISM, nothing seems to happen

When I try to compile PRISM, I get errors of the form:
Unexpected end of line seen...
or:
make: Fatal error in reader: Makefile, line 58: Unexpected end of line seen...

When I try to compile PRISM, I get an error of the form:
./setup.sh: line 33: syntax error: unexpected end of file

When I try to compile PRISM, I get an error of the form:
Assembler messages: Fatal error: can't create ../../obj/dd/dd_abstr.o: No such file or directory

When I try to compile PRISM, I get errors of the form:
dirname: extra operand `Files/Java/jdk1.5.0_09/bin/javac' Try `dirname --help' for more information.

When I try to compile PRISM, I get an error of the form:
/bin/sh: line 43: [: :/cygdrive/c/Program: binary operator expected...

Do I have to use GNU make to build PRISM?

Can I build PRISM on operating systems other than those currently supported?

---

Other issues

How do I uninstall PRISM?

I still have a problem installing/running PRISM. What can I do?

---

The PRISM Language

---

Introduction

In order to construct and analyse a model with PRISM, it must be specified in the PRISM language, a simple, state-based language, based on the Reactive Modules formalism of Alur and Henzinger [AH99]. In this section, we describe the PRISM language and present a number of small illustrative examples. A precise definition of the semantics of the language is available from the "Documentation" section of the PRISM web site. One of the best ways to learn what can be done with the PRISM language is to look at some existing examples. A number of these are included with the tool distribution in the examples directory. Many additional examples can be found on the "Case Studies" section of the PRISM website.

The fundamental components of the PRISM language are modules and variables. A model is composed of a number of modules which can interact with each other. A module contains a number of local variables. The values of these variables at any given time constitute the state of the module. The global state of the whole model is determined by the local state of all modules. The behaviour of each module is described by a set of commands. A command takes the form:

The guard is a predicate over all the variables in the model (including those belonging to other modules). Each update describes a transition which the module can make if the guard is true. A transition is specified by giving the new values of the variables in the module, possibly as a function of other variables. Each update is also assigned a probability (or in some cases a rate) which will be assigned to the corresponding transition.

---

Example 1

We will use the following simple example to illustrate the basic concepts of the PRISM language. Consider a system comprising two identical processes which must operate under mutual exclusion. Each process can be in one of 3 states: {0,1,2}. From state 0, a process will move to state 1 with probability 0.2 and remain in the same state with probability 0.8. From state 1, it tries to move to the critical section: state 2. This can only occur if the other process is not in its critical section. Finally, from state 2, a process will either remain there or move back to state 0 with equal probability. The PRISM code to describe this system can be seen below. In the next sections, we explain each aspect of the code in turn.

The PRISM Language: Example 1

---

Model Type

The PRISM language can be used to describe three types of probabilistic models: discrete-time Markov chains (DTMCs), continuous-time Markov chains (CTMCs) and Markov decision processes (MDPs). To indicate which type is being described, a PRISM model includes one of the keywords dtmc, ctmc or mdp. This is typically at the very start of the file (as in Example 1), but can actually occur anywhere in the file (except inside modules and other declarations). The keywords probabilistic, stochastic and nondeterministic can be used as alternatives for dtmc, dtmc and mdp, respectively. If no such model type declaration is included, the model is by default assumed to be an MDP.

---

Modules And Variables

The previous example uses two modules, M1 and M2, one representing each process. A module is specified as:

The definition of a module contains two parts: its variables and its guards. In this example, each module has one integer variable with range [0..2]. A variable declaration looks like:

Notice that the initial value of the variable is also specified. See the next subsection for more information about this subject. Boolean variables can also be used, e.g.:

The names given to modules and variables are referred to as identifiers. Identifiers can be made up of letters, digits and the underscore character, but cannot begin with a digit, i.e. they must satisfy the regular expression [A-Za-z_][A-Za-z0-9_]*, and are case-sensitive. Furthermore, identifiers cannot be any of the following, which are all reserved keywords in PRISM: bool, C, ceil, const, ctmc, double, dtmc, endinit, endmodule, endrewards, endsystem, F, false, floor, formula, G, global, I, init, int, label, max, mdp, min, module, nondeterministic, P, Pmin, Pmax, prob, probabilistic, R, rate, rewards, Rmin, Rmax, S, stochastic, system, true, U, X.

---

Initial States

The state space of a probabilistic model described in the PRISM language is the set of all possible valuations of its variables. The set of initial states of the model can be specified in one of two ways. The most common approach is simply to specify an initial value for each variable in the model. This is done in the declaration of each variable, as illustrated in Example 1 and as discussed in the previous section. If the initial value of a variable is omitted from its declaration, it is taken to be the minimum value of the variable's range.

This approach results in a single initial state. It is also possible to construct a model with multiple initial states. This is done using the init...endinit construct, which can be placed anywhere in the file except within a module definition, and removing any initial values from variable declarations. Between the init and endinit keywords, there should be a predicate over all the variables of the model. Any state which satisfies this predicate is an initial state.

Consider Example 1. As it stands, there is a single initial state (0,0) (i.e. x=0 and y=0). If we remove the init 0 part of both variable declarations and add the following to the end of the file:

there will be three initial states: (0,0), (0,1) and (0,2). Similarly, we could instead add:

in which case there would be two initial states: (0,1) and (1,0).

---

Commands

The behaviour of each module is described by commands, comprising a guard and one or more updates. The first command of module M1 in our example is:

The guard x=0 indicates that this describes the behaviour of the module when the variable x has value 0. The updates (x'=0) and (x'=1) and their associated probabilities state that the value of x will remain at 0 with probability 0.8 and change to 1 with probability 0.2. For DTMCs and MDPs, we require that the probabilities on the right hand side of a command sum to one. The second command:

illustrates that guards can contain constraints on any variable, not just the ones in that module, i.e. the behaviour of one module can depend on the state of another. Updates, however, can only specify values for variables belonging to the module. The command above also shows that, when there is a single update with probability 1, the 1.0: can be omitted.

If a module has more than one variable, updates describe the new value for each of them. For example, if it had two variables x1 and x2, a possible command would be:

Notice that elements of the updates are concatenated with & and that each element must be bracketed individually. If an update does not give a new value for a local variable, it is assumed not to change. As a special case, the keyword true can be used to denote an update where no variable's value changes.

---

Parallel Composition

The probabilistic model corresponding to a PRISM language description is constructed as the parallel composition of its modules. In every state of the model, there is a set of commands (belonging to any of the modules) which are enabled, i.e. whose guards are satisfied in that state. The choice between which command is performed (i.e. the scheduling) depends on the model type. For an MDP, as in Example 1, the choice is nondeterministic. By way of example, consider state (0,0) (i.e. x=0 and y=0). In the MDP, there would be a nondeterministic choice between two probability distributions:

• 0.8:(0,0) + 0.2:(1,0) (module M1 moves)
• 0.8:(0,0) + 0.2:(0,1) (module M2 moves)

For a DTMC, the choice is probabilistic: each enabled command is selected with equal probability. If Example 1 was a DTMC, then in state (0,0) of the model the following probability distribution would result:

• 0.8:(0,0) + 0.1:(1,0) + 0.1:(0,1)

For a CTMC, the choice is modelled as a "race" between transitions.

---

Local Nondeterminism

PRISM models which are MDPs can also exhibit local nondeterminism, which allows the modules themselves to make nondeterministic choices. In Example 1, we can make the probabilistic choice in the first state of module M1 nondeterministic by replacing the command:

with the commands:

Assuming we do the same for module M2, in state (0,0) of the MDP there will be a nondeterministic choice between three (trivial) probability distributions:

• 1.0:(0,0)
• 1.0:(1,0)
• 1.0:(0,1)

PRISM also permits local nondeterminism in models which are DTMCs, although the nondeterministic choice is randomised when the parallel composition of the modules occurs. Since the appearance of nondeterminism in a DTMC is often the result of a user error in the model specification, PRISM displays a warning when local nondeterminism is detected in a DTMC.

---

Module Renaming

PRISM also supports module renaming, which allows duplication of modules. In Example 1, module M2 is identical to module M1 so we can in fact replace its entire definition with:

Note that this renaming is done at a textual level, so any identifiers (including action labels) used in the module definition can be changed in this way. All of the variables in the module being renamed (in this case, just x) must be renamed to new, unused names.

---

Example 2

We now introduce a second example, which is a model of an N-place queue of jobs and a server which removes jobs from the queue and processes them. The PRISM code can be found below.

The PRISM Language: Example 2

As can be seen from the start of the file, the model is a continuous-time Markov chain (CTMC). One of the main differences, therefore, is that transitions of modules are labelled with (positive-valued) rates, rather than probabilities. The notation used in commands, however, to associate rates to transitions is identical to that used to assign probabilities in DTMCs and MDPs:

Example 2 also introduces a number of other PRISM language concepts: constants, action labels and synchronisation. These are described in the following sections.

---

Constants

PRISM also supports the use of constants, as seen in Example 2. Constants can be integers, doubles or Booleans and can be defined using literal values or as constant expressions (including in terms of each other) using the const keyword. For example:

The identifiers used for their names are subject to the same rules as variables.

Constants can be used anywhere that a constant value would be expected, such as the lower or upper range of a variable (e.g. N in Example 2), the probability or rate associated with an update (mu in Example 2), or anywhere in a guard or update. As will be described later constants can also be left undefined and specified later, either to a single value or a range of values, using experiments.

Note: For the sake of backward-compatibility, the notation used in earlier versions of PRISM (const for const int and rate or prob for const double) is still supported.

---

Expressions

The definition of the area constant, in the example above, uses an expression. We now define more precisely what types of expression are supported by PRISM. Expressions can contain literal values (12, 3.141592, true, false, etc.), identifiers (corresponding to variables, constants, etc.) and operators from the following list:

• *, / (multiplication, division)
• +, - (addition, subtraction)
• <, <=, >=, > , =, != (relational operators)
• ! (not)
• & (and)
• | (or)
• ? (condition evaluation: condition ? a : b means "if condition is true then a else b")

All of these operators except ? are left associative (i.e. they are evaluated from left to right). The precedence of the operators is as found in the list above, most strongly binding operators first. Operators on the same line (e.g. + and -) are of equal precedence.

The notation for expressions is hence essentially equivalent to that of C/C++ or Java. One notable exception to this is that the division operator / always performs floating point, not integer, division, i.e. the result of 22/7 is 3.142857... not 3. All expressions must evaluate correctly in terms of type (integer, double or Boolean).

Ranges

A shorthand notation for describing ranges is also supported. For example:

is equivalent to:

All the elements of such an expression (x, 1, 5, etc.) can themselves be expressions. Replacing the = with an != is equivalent to negating the whole expression. So, for example:

is equivalent to:

Built-in Functions

Expressions can make use of several built-in functions, which are accessed via the func keyword. Currently, the supported functions are: min and max, which select the minimum and maximum value, respectively, of two or more numbers; floor and ceil, which round down and up, respectively, to the nearest integer; pow which raises one number to the power of another; and mod for integer modulo operations. The format is:

Examples of their usage are:

For compatability with older versions of PRISM, min, max,floor and ceil can still be used directly, e.g. max(a,b,c).

Use of Expressions

Expressions can be used in a wide range of places in a PRISM language description, e.g.:

• constant definitions
• lower/upper bounds and initial values for variables
• guards
• probabilities/rates
• updates

This allows, for example, the probability in a command to be dependent on the current state:

---

Synchronisation

Another feature of PRISM introduced in Example 2 is synchronisation. In the style of many process algebras, we allow commands to be labelled with actions. These are placed inside the square brackets which mark the start of the command, for example serve in this command from Example 2:

These actions can be used to force two or more modules to make transitions simultaneously (i.e. to synchronise). For example, in state (3,0) (i.e. q=3 and s=0), the composed model can move to state (2,1), synchronising over the serve action. The rate of this transition is equal to the product of the two individual rates (in this case, lambda * 1 = lambda). The product of two rates does not always meaningfully represent the rate of a synchronised transition. A common technique, as seen here, is to make one action passive, with rate 1 and one action active, which actually defines the rate for the synchronised transition. By default, all modules are combined using the standard CSP parallel composition (i.e. modules synchronise over all their common actions).

---

Process Algebra Operators

To make the concept of synchronisation described above more powerful, PRISM allows you to define precisely the way in which the set of modules are composed in parallel. This is specified using the system ... endsystem construct, placed at the end of the model description, which should contain a process-algebraic expression. This expression should feature each module exactly once, and can use the following (CSP-based) operators:

• M1 || M2 : full parallel composition of modules M1 and M2 (synchronising on all actions which appear in both M1 and M2)
• M1 ||| M2 : asynchronous parallel composition of M1 and M2 (fully interleaved, no synchronisation)
• M1 |[a,b,...]| M2 : restricted parallel composition of modules M1 and M2 (synchronising only on actions from the set {a, b,...})
• M / {a,b,...} : hiding of actions {a, b, ...} in module M
• M {a<-b,c<-d,...} : renaming of actions a to b, c to d, etc. in module M.

The first two types of parallel composition (|| and |||) are associative and can be applied to more than two modules at once. When evaluating the expression, the hiding and renaming operators bind more tightly than the three parallel composition operators. No other rules of precedence are defined and parentheses should be used to specify the order in which modules are composed.

Some examples of expressions which could be included in the system ... endsystem construct are as follows:

• (station1 ||| station2 ||| station3) |[serve]| server
• ((P1 |[a]| P2) / {a}) || Q
• ((P1 |[a]| P2) {a<-b}) |[b]| Q

When no parallel composition is specified by the user, PRISM implicitly assumes an expression of the form M1 || M2 || ... containing all of the modules in the model. For a more formal definition of the process algebra operators described above, check the semantics of the PRISM language, available from the "Documentation" section of the PRISM web site.

PRISM is also able to import model descriptions written in (a subset of) the stochastic process algebra PEPA [Hil96].

---

Global Variables

In addition to the local variables belonging to each module, a PRISM model can also include global variables, which can be written to, as well as read, by all modules. Like local variables, these can be integers or Booleans. Global variables are declared in identical fashion to a module's local variables, except that the declaration must not be inside the definition of any module. Some example declarations are as follows:

A global variable can be modified by any module and provides another way for modules to interact. An important restriction on the use of global variables is the fact that commands which synchronise with other modules (i.e. those with an action label attached; see the section "Synchronisation") cannot modify global variables. PRISM will detect this and report an error.

---

Formulas And Labels

PRISM models can include formulas which are used to avoid duplication of code. A formula comprises a name (an identifier) and an expression. The formula name can then be used as shorthand for the expression anywhere an expression might usually be accepted. A formula is defined as follows:

It can then be used anywhere within that file, as for example in this command:

The effect is exactly as if the following had been typed:

Formulas defined in a model can also be used when specifying its properties.

Formulas and renaming

During parsing of the model, expansion of formulas is done before module renaming so, if a module which uses formulas is renamed to another module, it is the contents of the formula which will be renamed, not the formula itself.

Labels

PRISM models can also contain labels. These are are a way of identifying sets of states that are of particular interest. Labels can only be used when specifying properties but, for convenience, can be defined in model files as well as property files.

Labels differ from formulas in two other ways: firstly, they must be of Boolean type; secondly, they are written using quotation marks ("..."), as illustrated in the following example:

---

PRISM Language Files

Files containing model descriptions written in the PRISM language can contain any amount of white space (spaces, tabs, new lines, etc.), all of which is ignored when the file is parsed by the tool. Comments can also be used included in files in the style of the C programming language, by preceding them with the characters //. This is illustrated by the PRISM language examples from earlier in this section. By convention, PRISM model files which describe MDPs, DTMCs and CTMCs are given the extensions .nm, .pm and .sm, respectively.

---

Costs And Rewards

PRISM now includes support for the specification and analysis of properties based on costs and rewards. This means that PRISM can be used to reason, not just about the probability that a model behaves in a certain fashion, but about a wider range of quantitative measures relating to model behaviour. For example, PRISM can be used to compute properties such as "expected time", "expected number of lost messages" or "expected power consumption". The implementation of cost- and reward-based techniques in the tool is only partially completed and is still ongoing. If you have questions, comments or feature-requests relating to this functionality, please feel free to contact the PRISM team about this.

The basic idea is that probabilistic models (of all three types) developed in PRISM can be augmented with costs or rewards: real values associated with certain states or transitions of the model. In fact, since there is no practical distinction between costs and rewards (except that costs are generally perceived to be "bad" and rewards to be "good"), PRISM only supports rewards. The user is, however, free to interpret the values however they choose.

In this section, we describe how models described in the PRISM language can be augmented with rewards. Later, we will discuss how to express properties that relate to these rewards. Rewards are associated with models using rewards ... endrewards constructs, which can appear anywhere in a model file except within a module definition. These constructs contains one or more reward items. Consider the following simple example:

This assigns a reward of 1 to every state of the model. It comprises a single reward item, the left part of which (true) is a guard and the right part of which (1) is a reward. States of the model which satisfy the predicate in the guard are assigned the corresponding reward. More generally, state rewards can be specified using multiple reward items, each of the form guard : reward;, where guardis a predicate (over all the variables of the model) and reward is an expression (containing any variables, constants, etc. from the model). For example:

assigns a reward of 100 to states satisfying x=0 or x=10 and a reward of 2*x to states satisfying x>0 & x<10. Note that a single reward item can assign different rewards to different states, depending on the values of model variables in each one. Any states which do not satisfy the guard of any reward item will have no reward assigned to them. For states which satisfy multiple guards, the reward assigned to the state is the sum of the rewards for all the corresponding reward items.

Rewards can also be assigned to transitions of a model. These are specified in a similar fashion to state rewards, within the rewards ... endrewards construct. Reward items describing transition rewards are of the form [action] guard : reward;, the interpretation being that transitions from states which satisfy the guard guard and are labelled with the action action acquire the reward reward. For example:

assigns a reward of 1 to all transitions in the model with no action label, and rewards of x and 2*x to all transitions labelled with actions a and b, respectively.

As is the case for states, multiple reward items can specify rewards for a single transition, in which case the resulting reward is the sum of all the individual rewards. A model description can specify rewards for both states and transitions. These are all placed together in a single rewards...endrewards construct.

A PRISM model can have multiple reward structures. Optionally, these can be given labels such as in the following example:

---

Property Specification

---

Introduction

In order to analyse a probabilistic model which has been specified and constructed in PRISM, it is necessary to identify one or more properties of the model which can be evaluated by the tool. As is typically the case with formal verification techniques, in PRISM this is done using temporal logic. More specifically, properties are expressed in a language based on the logics PCTL (for DTMCs and MDPs) and CSL (for CTMCs), probabilistic extensions of the classical temporal logic CTL. In fact, PRISM supports numerous additional customisations and extensions of these two logics. Full details of the property specifications permitted in PRISM are provided in the following sections. For the precise syntax and semantics of the original two logics, see [HJ94],[BdA95] for PCTL and [ASSB96],[BKH99] for CSL.

Before discussing property specifications in detail, it is perhaps instructive to first illustrate some typical examples of properties which PRISM can handle. The following are a selection of such properties. In each case, we give both the PRISM syntax and a natural language translation:

"the algorithm eventually terminates successfully with probability 1"

"from an initial state, the probability that more than 5 errors occur within the first 100 time units is less than 0.1"

"when a shutdown occurs, the probability of system recovery being completed in between 1 and 2 hours without further failures occurring is greater than 0.75"

"in the long-run, the probability that an inadequate number of sensors are operational is less than 0.01"

Note that the above properties are all assertions, i.e. ones to which we would expect a "yes" or "no" answer. This is because all references to probabilities are associated with an upper or lower bound which can be checked to be either true or false. In PRISM, we can also directly specify properties which evaluate to a numerical value, e.g.:

"the probability that process 1 terminates before process 2 does"

"the maximum probability that more than 10 messages have been lost by time T"

"the long-run probability that the queue is more than 75% full"

Furthermore, PRISM makes it easy to compute the values of such properties for a range of parameters and plot graphs of the results using experiments. This is often a very useful way of identifying interesting patterns or trends in the behaviour of a system. See the Case Studies section of the PRISM website for many examples of this kind of analysis.

---

Identifying A Set Of States

One of the most fundamental tasks when specifying properties of a model is to identify particular sets or classes of states of the model. For example, to verify a property such as "the algorithm eventually terminates successfully with probability 1", it is first necessary to identify the states of the model which correspond to situations where "the algorithm has terminated successfully".

In PRISM, this is achieved simply by writing an expression in the PRISM language which evaluates to a Boolean value. This expression will typically contain references to variables (and constants) from the model to which it relates. The set of states corresponding to this expression is those for which it evaluates to "true". Returning to our example above, the property "the algorithm has terminated successfully" might be represented, for instance, by the PRISM language expression program_counter=10 & num_errors=0. In terms of the way temporal logics are usually presented, these expressions correspond to atomic propositions.

---

Basic Syntax

The basic syntax of the language for expressing a PRISM property prop is given by the following grammar:

where:

• expr is a PRISM language expression which evaluates to a Boolean (as described in the previous section),
• p is a PRISM language expression evaluating to a double in the range [0,1],
• t is a PRISM language expression evaluating to a non-negative double or integer.

A property is evaluated with respect to a single state of a model. For the syntax given above, all properties evaluate to Boolean values, i.e. for any state $s$ of a model, a property is either "true" or "false" in that state. Equivalently, we also say that a property is "satisfied" or "not satisfied" in a state. For the basic operators of the logic (i.e. true, false, expr, !, &, | and =>) the semantics are as for classical propositional logic:

• true is true in all states,
• false is not true in any state,
• expr is true if the PRISM expression expr evaluates to true,
• !prop is true if prop is not true,
• prop1 & prop2 is true if both prop1 and prop2 are true,
• prop1 | prop2 is true if either prop1 or prop2 is true,
• prop1 => prop2 is true if prop1 implies prop2.

---

The P Operator

The two other principal operators for specifying properties are the P and S operators. The P operator is applicable to all three model types. It allows us to reason about the probability that a certain type of behaviour is observed. Informally, the property:

is true in a state s of a DTMC, MDP or CTMC if "the probability that path property pathprop is satisfied by the paths from state s meets the bound bound". A typical example of a bound would be:

which means: "the probability that path property pathprop is satisfied by the paths from state s is greater than 0.98". The types of path property supported by PRISM and their semantics are discussed below.

For a DTMC, the probability measure of the set of paths from a state s which satisfy a path property pathprop is well-defined; see e.g. [HJ94]. Similarly, for a CTMC, the probability measure for such a set of paths can also be defined; see e.g. [BKH99].

For MDPs, however, a probability measure can only be feasibly defined once all nondeterminism has been removed. Hence, the actual meaning of the property P bound [ pathprop ] for an MDP is taken to be "the probability that path property pathprop is satisfied by the paths from state s meets the bound bound for all possible resolutions of nondeterminism". This means that, for an MDP, properties using the P operator actually reason about the minimum or maximum probability, over all possible resolutions of nondeterminism, that a certain type of behaviour is observed. This depends on the bound attached to the P operator: a lower bound (> or >=) relates to minimum probabilities and an upper bound (< or <=) to maximum probabilities. For more details on this, see e.g. [BK98].

Path properties

As illustrated in the earlier syntax definition, various different types of path property can be used inside the P operator.

• X : "next"
• U : "until"
• F : "eventually" (sometimes called "future", "finally", or "forwards")
• G : "always" (sometimes called "globally")

as well as bounded variants of the last three:

• U time
• F time
• G time

A path property is evaluated to either true or false for a single path in a model. In the following sections, we describe the semantics for each of the three types of path property.

"Next" path properties

The property X prop is true for a path if prop is true in its second state, An example of this type of property, used inside a P operator, is:

which is true in a state if "the probability of the expression y=1 being true in the next state is less than 0.01".

"Until" path properties

The property prop1 U prop2 is true for a path if prop2 is true in some state of the path and prop1 is true in all preceding states. A common application of this type of property is the case where prop1 is true. A simple example of this would be:

which is true in a state if "the probability that z is eventually equal to 2, and that z remains less than 2 up until that point, is greater than 0.5".

"Eventually" path properties

The property F prop is true for a path if prop eventually becomes true at some point along the path. The F operator is in fact a special case of the U operator (you will often see F prop written as true U prop). A simple example is:

which is true in a state if "the probability that z is eventually greater than 2is less than 0.1".

"Globally" path properties

Whereas the F operator is used for "reachability" properties, G represents "invariance". The property G prop is true of a path if prop remains true at all states along the path. Thus, for example:

states that, with probability at least 0.99, z never exceeds 10.

"Bounded" variants of path properties

The "bounded" variants of U, F and G path properties are generalisations where an additional bound is imposed on the property being satisfied. Since in DTMCs and MDPs, time progresses in discrete steps, whereas CTMCs model real (continuous) time, we treat these two cases separately for this operator.

For a DTMC or MDP, the time interval specification time must be of the form "<=t" where t is a PRISM expression evaluating to a non-negative integer. A bounded until property prop1 U<=t prop2, for example, is satisfied along a path if prop2 becomes true within t steps and prop1 is true in all states before that point. A typical example of this would be:

which is true in a state if "the probability of y first exceeding 3 within 7 time steps is greater than or equal to 0.98". Similarly:

is true in a state if "the probability of y being equal to 4 within 7 time steps is greater than or equal to 0.98" and:

is true if the probability of y staying equal to 4 for 7 time steps is at least 0.98.

In the context of a CTMC, the time interval specification time can take any of the three forms: >=t, <=t or [t1,t2], where t, t1 and t2 are PRISM expression evaluating to a non-negative doubles, and t1 is no greater than t2. In each case, time defines an interval of real values in which the path property must be true.

For example:

means that the probability of y being greater than 1 within 6.5 time-units (and remaining less than or equal to 1 at all preceding time-points) is at least 0.25.

states that the probability of y exceeding 1 at some point after 5.5 time-units have elapsed is less than 0.4, and:

says that the probability that y exceeds 1 for the whole time interval [5.5,6.5] is greater than zero".

Transient probabilities

We can also use the bounded F operator to refer to a single time instant, e.g.:

refers to the probability of y being 6 at time instant 10.

---

The S Operator

The S operator is used to reason about the steady-state behaviour of a model, i.e. its behaviour in the long-run or equilibrium. Although this could in principle relate to all three model types, PRISM currently only provides support for CTMCs. The definition of steady-state (long-run) probabilities for finite CTMCs is well defined (see e.g. [Ste94]). Informally, the property:

is true in a state s of a CTMC if "starting from s, the steady-state (long-run) probability of being in a state which satisfies prop, meets the bound bound". A typical example of this type of property would be:

which means: "the long-run probability of the queue being more than 75% full is less than 0.05".

---

Satisfaction Of Properties

All of the properties described in the previous sections evaluate to a Boolean value. Although the satisfaction of a property is defined in terms of a single state, when analysing a property of a model, PRISM considers the property to be true if it is satisfied in all states of the model, and false otherwise.

To check if a property is satisfied in some subset of states, for example just the initial states, properties can be prefixed with an implication, e.g.:

See the section "Properties Files" for details of the "init" expression.

---

Determining The Actual Probability

As discussed earlier, it is often useful to know the actual probability that some behaviour of a model is observed, rather than just whether or not the probability is above or below a given bound. Hence, PRISM allows properties of the following form:

The arguments to these operands, either a path property for P or another property for S, are exactly as before; the only difference is that the probability bound is removed. These properties return a numerical rather than a Boolean value.

Note that the probability bound on a P or S operator can only be replaced with =? if it is the outermost operator of the property in which it appears; otherwise the semantics are not well defined. Note also that, for MDPs, the situation is slightly more complex. Probabilities for an MDP can only be computed once the nondeterminism has been resolved. Hence, PRISM actually computes either the minimum or maximum probability of a path property being satisfied, quantifying over all possible resolutions (i.e. the best and worst cases). Therefore, for MDPs we have two possible types of property:

which return the minimum and maximum probabilities, respectively.

All of these operators return a single numerical value. In the simplest case, where the model being verified has a single initial state, the numerical value returned is the one corresponding to that state. Hence, for example:

returns the probability of, from the initial state, reaching a state satisfying x=5&y=5. It is also possible, however, to obtain the probability for an arbitrary state, by specifying an atomic proposition, true only in that state, inside braces ({...}) before the closing ] bracket. This is known as a filter. For example, if the model contains two variables, X and y, then:

returns the probability of, from the state (1,2) (i.e. x=1 and y=2), reaching a state satisfying x=5&y=5. It is possible of course that the expression in the filter satisfies more than one state. If this the case, by default the first such state (lexicographically) is chosen. In this situation, PRISM will display a warning to notify you that the expression in the filter matched multiple states and will display what the first matching state is. The same approach is taken in the situation where no filter is given but the model contains multiple initial states. In this case, the numerical result obtained is for the first (lexicographically speaking) of the set of initial states. Note that if the expression in the filter is not satisfied by any states of the model, an error is reported.

It is also possible to possible to request either the minimum and maximum value from a set of values. For example:

return the minimum and maximum probability, respectively, of reaching a state satisfying x=5&y=5 from all the states satisfying y=2. In addition, PRISM will report the states of the model in which the minimum or maximum probability is attained. You can in fact also request that both the minimum and maximum value are computed simultaneously using, for example, {y=2}{min}{max}. In this case, both values will be reported, but the actual return value of the property will be the minimum value.

Finally, filters can also be used for conventional P and S properties. This has no bearing on the result of model checking a property; it simply causes the probabilities (where non-zero) for all states satisfying the expression in the filter to be printed during model checking. For example:

will return a Boolean value, depending whether the property is true in all states of the model or not, but the probability (where non-zero) of path property true U x=5&y=5 being satisfied will be displayed for all states where y=2.

---

Properties Files

Files containing properties to be analysed by PRISM can also contain constants, as is the case for model files. These are defined in identical fashion, for example:

As before, these constants can actually be left undefined and then later assigned either a single value or a range of values using experiments.

In fact, probability bounds for the P or S operators (like P above) and upper or lower bounds for the U operator (like T above) can be arbitrary expressions, provided they are constant. Furthermore, expressions in the properties file can also refer to constants previous defined in the model file.

Another feature of properties files is labels. These are a way of defining sets of states that will be referred to in properties (they correspond to atomic propositions in a temporal logic setting). As described earlier, labels can be defined in either model files or property files.

Labels are defined using the keyword label, followed by a name (identifier) in double quotes, and then an expression which evaluates to a Boolean. Definition and usage of formulas are illustrated in the following example:

Two special cases are the "init" and "deadlock" labels which are always defined. Thes are true in initial states of the model and states where deadlocks were found (and fixed by adding self-loops), respectively. The former is useful if you only wish to to check whether a property is true in the initial states, e.g.:

A PRISM properties file can contain any number of properties. Like model files, they can also include any amount of white space (spaces, tabs, new lines, etc.) and C-style comments, which are both ignored. By convention, files are given the extension .pctl for properties of DTMCs and MDPs and extension .csl for properties of CTMCs.

---

Specification Of Reward-based Properties

PRISM models can be augmented with information about rewards (or costs). The tool can analyse properties which relate to the expected values of these rewards. This is achieved using the R operator, which works in a similar fashion to the P and S operators, and can be used either in a Boolean-valued query, e.g.:

where bound takes the form <r, <=r, >r or >=r for an expression r evaluating to a non-negative double, or a real-valued query, e.g.:

where query is =? for a DTMC or CTMC, and min=? or max=? for MDPs.

Informally, "R bound [ rewardprop ]" is true in a state of a model if "the expected reward associated with rewardprop of the model when starting from that state'' meets the bound bound and "R query [ rewardprop ]" returns the actual expected reward value.

There are four different types of reward properties, namely:

• "reachability reward": F prop
• "cumulative reward" : C<=t
• "instantaneous reward" : I=t
• "steady-state reward" : S.

Below, we consider each of these cases in turn. The descriptions here are kept relatively informal. For precise definitions (in the case of DTMCs and CTMCs), see [KNP07a].

"Reachability reward" properties

"Reachability reward" properties associate a reward with each path of a model. More specifically, they refer to the reward accumulated along a path until a certain point is reached. The manner in which rewards are accumulated depends on the model type. For DTMCs and MDPs, the total reward for a path is the sum of the state rewards for each state along the path plus the sum of the transition rewards for each transition between these states. The situation for CTMCs is similar, except that the state reward assigned to each state of the model is interpreted as the rate at which rewards are accumulated in that state, i.e. if t time units are spent in a state with state reward r, the reward accumulated in that state is r x t. Hence, the total reward for a path in a CTMC is the sum of these products for each state along the path plus the sum of the transition rewards for each transition between these states.

The reward property "F prop" corresponds to the reward cumulated along a path until a state satisfying property prop is reached, where rewards are cumulated as described above. State rewards for the prop-satisfying state reached are not included in the cumulated va