AllOnOnePage.html 97.7 KB
edit raw blame history

<!DOCTYPE HTML PUBLIC "-//W3C//DTD HTML 4.01 Transitional//EN"
"http://www.w3.org/TR/html4/loose.dtd">

<html>
<head>

<title>
PRISM Manual | PropertySpecification / AllOnOnePage
</title>

<meta http-equiv="Content-Type" content="text/html; charset=UTF-8">
<meta name="keywords" content="prism, probabilistic, symbolic, model, checker, verification, birmingham, oxford, parker, norman, kwiatkowska">

<link rel="icon" href="../pub/skins/offline/images/p16.ico" type="image/x-icon">
<link rel="shortcut icon" href="../pub/skins/offline/images/p16.ico" type="image/x-icon">

<!--HTMLHeader--><style type='text/css'><!--
  ul, ol, pre, dl, p { margin-top:0px; margin-bottom:0px; }
  code.escaped { white-space: nowrap; }
  .vspace { margin-top:1.33em; }
  .indent { margin-left:40px; }
  .outdent { margin-left:40px; text-indent:-40px; }
  a.createlinktext { text-decoration:none; border-bottom:1px dotted gray; }
  a.createlink { text-decoration:none; position:relative; top:-0.5em;
    font-weight:bold; font-size:smaller; border-bottom:none; }
  img { border:0px; }
  .editconflict { color:green;
  font-style:italic; margin-top:1.33em; margin-bottom:1.33em; }

  table.markup { border:2px dotted #ccf; width:90%; }
  td.markup1, td.markup2 { padding-left:10px; padding-right:10px; }
  table.vert td.markup1 { border-bottom:1px solid #ccf; }
  table.horiz td.markup1 { width:23em; border-right:1px solid #ccf; }
  table.markup caption { text-align:left; }
  div.faq p, div.faq pre { margin-left:2em; }
  div.faq p.question { margin:1em 0 0.75em 0; font-weight:bold; }
  div.faqtoc div.faq * { display:none; }
  div.faqtoc div.faq p.question
    { display:block; font-weight:normal; margin:0.5em 0 0.5em 20px; line-height:normal; }
  div.faqtoc div.faq p.question * { display:inline; }

    .frame
      { border:1px solid #cccccc; padding:4px; background-color:#f9f9f9; }
    .lfloat { float:left; margin-right:0.5em; }
    .rfloat { float:right; margin-left:0.5em; }
a.varlink { text-decoration:none; }

.sourceblocklink {
  text-align: right;
  font-size: smaller;
}
.sourceblocktext {
  padding: 0.5em;
  border: 1px solid #808080;
  color: #000000;
  background-color: #f1f0ed;
}
.sourceblocktext div {
  font-family: monospace;
  font-size: small;
  line-height: 1;
  height: 1%;
}
.sourceblocktext div.head,
.sourceblocktext div.foot {
  font: italic medium serif;
  padding: 0.5em;
}

--></style>  <meta name='robots' content='index,follow' />


<link type="text/css" rel="stylesheet" href="../pub/skins/offline/css/base.css">
<link type="text/css" rel="stylesheet" href="../pub/skins/offline/css/prism.css">
<link type="text/css" rel="stylesheet" href="../pub/skins/offline/css/prismmanual.css">

</head>

<body text="#000000" bgcolor="#ffffff">

<div id="layout-maincontainer">
<div id="layout-main">

<div id="prism-mainbox">

<!-- ============================================================================= -->

<!--PageHeaderFmt-->
<!--/PageHeaderFmt-->

<!--PageTitleFmt--><!--PageText-->
<div id='wikitext'>
<div class='vspace'></div><h1><span class='big'>Property Specification</span></h1>
<hr />
<h1>Introduction</h1>
<p>In order to analyse a probabilistic model which has been specified and constructed in PRISM,
it is necessary to identify one or more <em>properties</em> of the model
which can be evaluated by the tool.
PRISM's <em>property specification language</em> subsumes several well-known probabilistic temporal logics, including PCTL, CSL, probabilistic LTL and PCTL*.
PCTL is used for specifying properties of DTMCs, MDPs or PTAs;
CSL is an extension of PCTL for CTMCs;
LTL and PCTL* can be used to specify properties of
DTMCs and MDPs (or untimed properties of CTMCs).
PRISM also supports most of the (non-probabilistic) temporal logic CTL.
</p>
<p class='vspace'>In fact, PRISM also 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. The presentation given here is relatively informal. For the precise syntax and semantics of the various logics, see [<a class='wikilink' href='../Main/References.html#HJ94'>HJ94</a>],[<a class='wikilink' href='../Main/References.html#BdA95'>BdA95</a>] for PCTL, [<a class='wikilink' href='../Main/References.html#ASSB96'>ASSB96</a>],[<a class='wikilink' href='../Main/References.html#BKH99'>BKH99</a>] for CSL and, for example, [<a class='wikilink' href='../Main/References.html#Bai98'>Bai98</a>] for LTL and PCTL*. You can also find various pointers to useful papers in the <a class='urllink' href='http://www.prismmodelchecker.org/about.php'>About</a> and <a class='urllink' href='http://www.prismmodelchecker.org/doc/'>Documentation</a> sections of the PRISM website.
</p>
<p class='vspace'>Before discussing property specifications in more 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:
</p>
<div class='vspace'></div>
<div class='sourceblock ' id='sourceblock1'>
  <div class='sourceblocktext'><div class="prism"><span class="prismkeyword">P</span>&gt;=<span class="prismnum">1</span> [ <span class="prismkeyword">F</span> "<span class="prismident">terminate</span>" ]<br/>
</div></div>
  <div class='sourceblocklink'><a href='http://prismmodelchecker.localhost/manual/PropertySpecification/AllOnOnePage?action=sourceblock&amp;num=1' type='text/plain'>[&#036;[Get Code]]</a></div>
</div>

<p>"the algorithm eventually terminates successfully with probability 1"
</p>
<div class='vspace'></div>
<div class='sourceblock ' id='sourceblock2'>
  <div class='sourceblocktext'><div class="prism">"<span class="prismkeyword">P</span>&lt;<span class="prismnum">0.1</span> [ <span class="prismkeyword">F</span>&lt;=<span class="prismnum">100</span> <span class="prismident">num_errors</span> &gt; <span class="prismnum">5</span> ]<br/>
</div></div>
  <div class='sourceblocklink'><a href='http://prismmodelchecker.localhost/manual/PropertySpecification/AllOnOnePage?action=sourceblock&amp;num=2' type='text/plain'>[&#036;[Get Code]]</a></div>
</div>

<p>"the probability that more than 5 errors occur within the first 100 time units is less than 0.1"
</p>
<div class='vspace'></div>
<div class='sourceblock ' id='sourceblock3'>
  <div class='sourceblocktext'><div class="prism"><span class="prismkeyword">S</span>&lt;<span class="prismnum">0.01</span> [ <span class="prismident">num_sensors</span> &lt; <span class="prismident">min_sensors</span> ]<br/>
</div></div>
  <div class='sourceblocklink'><a href='http://prismmodelchecker.localhost/manual/PropertySpecification/AllOnOnePage?action=sourceblock&amp;num=3' type='text/plain'>[&#036;[Get Code]]</a></div>
</div>

<p>"in the long-run, the probability that an inadequate number of sensors are operational is less than 0.01"
</p>
<p class='vspace'>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.:
</p>
<div class='vspace'></div>
<div class='sourceblock ' id='sourceblock4'>
  <div class='sourceblocktext'><div class="prism"><span class="prismkeyword">P</span>=? [ !<span class="prismident">proc2_terminate</span> <span class="prismkeyword">U</span> <span class="prismident">proc1_terminate</span> ]<br/>
</div></div>
  <div class='sourceblocklink'><a href='http://prismmodelchecker.localhost/manual/PropertySpecification/AllOnOnePage?action=sourceblock&amp;num=4' type='text/plain'>[&#036;[Get Code]]</a></div>
</div>

<p>"the probability that process 1 terminates before process 2 does"
</p>
<div class='vspace'></div>
<div class='sourceblock ' id='sourceblock5'>
  <div class='sourceblocktext'><div class="prism"><span class="prismkeyword">Pmax</span>=? [ <span class="prismkeyword">F</span>&lt;=<span class="prismident">T</span> <span class="prismident">messages_lost</span> &gt; <span class="prismnum">10</span> ]<br/>
</div></div>
  <div class='sourceblocklink'><a href='http://prismmodelchecker.localhost/manual/PropertySpecification/AllOnOnePage?action=sourceblock&amp;num=5' type='text/plain'>[&#036;[Get Code]]</a></div>
</div>

<p>"the maximum probability that more than 10 messages have been lost by time <code>T</code>" (for an MDP/PTA)
</p>
<div class='vspace'></div>
<div class='sourceblock ' id='sourceblock6'>
  <div class='sourceblocktext'><div class="prism"><span class="prismkeyword">S</span>=? [ <span class="prismident">queue_size</span> / <span class="prismident">max_size</span> &gt; <span class="prismnum">0.75</span> ]<br/>
</div></div>
  <div class='sourceblocklink'><a href='http://prismmodelchecker.localhost/manual/PropertySpecification/AllOnOnePage?action=sourceblock&amp;num=6' type='text/plain'>[&#036;[Get Code]]</a></div>
</div>

<p>"the long-run probability that the queue is more than 75% full"
</p>
<p class='vspace'>Furthermore, PRISM makes it easy to combine such properties into more complex expressions,
compute their values for a range of parameters
and plot graphs of the results using <a class='wikilink' href='../RunningPRISM/Experiments.html'>experiments</a>.
This is often a very useful way of identifying interesting
patterns or trends in the behaviour of a system.
See the <a class='urllink' href='http://www.prismmodelchecker.org/casestudies/'>Case Studies</a> section of the <a class='urllink' href='http://www.prismmodelchecker.org/'>PRISM website</a> for many examples of this kind of analysis.
</p><hr />
<h1>Identifying A Set Of States</h1>
<p>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 terms of the way temporal logics are usually presented,
these correspond to <em>atomic propositions</em>.
</p>
<p class='vspace'>In PRISM, this is achieved simply by writing an <a class='wikilink' href='../ThePRISMLanguage/Expressions.html'>expression</a> 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 <code>true</code>. We say that the expression is "satisfied" in these states.
</p>
<p class='vspace'>For example, in the property given above:
</p>
<div class='vspace'></div>
<div class='sourceblock ' id='sourceblock7'>
  <div class='sourceblocktext'><div class="prism"><span class="prismkeyword">P</span>&lt;<span class="prismnum">0.1</span> [ <span class="prismkeyword">F</span>&lt;=<span class="prismnum">100</span> <span class="prismident">num_errors</span> &gt; <span class="prismnum">5</span> ]<br/>
</div></div>
  <div class='sourceblocklink'><a href='http://prismmodelchecker.localhost/manual/PropertySpecification/AllOnOnePage?action=sourceblock&amp;num=7' type='text/plain'>[&#036;[Get Code]]</a></div>
</div>

<p class='vspace'>the expression <code>num_errors &gt; 5</code> is used to identify states of the model where more than 5 errors have occurred.
</p>
<p class='vspace'>It is also common to use <a class='wikilink' href='../ThePRISMLanguage/FormulasAndLabels.html'>labels</a> to identify states in this way, like <code>"terminate"</code> in the example:
</p>
<div class='vspace'></div>
<div class='sourceblock ' id='sourceblock8'>
  <div class='sourceblocktext'><div class="prism"><span class="prismkeyword">P</span>&gt;=<span class="prismnum">1</span> [ <span class="prismkeyword">F</span> "<span class="prismident">terminate</span>" ]<br/>
</div></div>
  <div class='sourceblocklink'><a href='http://prismmodelchecker.localhost/manual/PropertySpecification/AllOnOnePage?action=sourceblock&amp;num=8' type='text/plain'>[&#036;[Get Code]]</a></div>
</div>

<p class='vspace'>Properties can refer to <a class='wikilink' href='../ThePRISMLanguage/FormulasAndLabels.html'>labels</a> either from the model to which the property relates, or included in the same <a class='wikilink' href='PropertiesFiles.html'>properties file</a>.
</p><hr />
<h1>The P Operator</h1>
<p>One of the most important operators in the PRISM property specification language is the <code><strong>P</strong></code> operator, which is used to reason about the probability of an event's occurrence. This operator was originally proposed in the logic PCTL but also features in the other logics supported by PRISM, such as CSL. The <code><strong>P</strong></code> operator is applicable to all types of models supported by PRISM.
</p>
<p class='vspace'>Informally, the property:
</p>
<div class='vspace'></div>
<div class='sourceblock ' id='sourceblock9'>
  <div class='sourceblocktext'><div class="prism"><span class="prismkeyword">P</span> <span class="prismident">bound</span> [ <span class="prismident">pathprop</span> ]<br/>
</div></div>
  <div class='sourceblocklink'><a href='http://prismmodelchecker.localhost/manual/PropertySpecification/AllOnOnePage?action=sourceblock&amp;num=9' type='text/plain'>[&#036;[Get Code]]</a></div>
</div>

<p class='vspace'>is true in a state <em>s</em> of a model if
"the probability that path property <code>pathprop</code> is satisfied by the paths from state <em>s</em>
meets the bound <code>bound</code>".
A typical example of a bound would be:
</p>
<div class='vspace'></div>
<div class='sourceblock ' id='sourceblock10'>
  <div class='sourceblocktext'><div class="prism"><span class="prismkeyword">P</span>&gt;<span class="prismnum">0.98</span> [ <span class="prismident">pathprop</span> ]<br/>
</div></div>
  <div class='sourceblocklink'><a href='http://prismmodelchecker.localhost/manual/PropertySpecification/AllOnOnePage?action=sourceblock&amp;num=10' type='text/plain'>[&#036;[Get Code]]</a></div>
</div>

<p class='vspace'>which means: "the probability that <code>pathprop</code> is satisfied by the paths from state <em>s</em> is greater than 0.98". More precisely, <code>bound</code> can be any of <code>&gt;=p</code>, <code>&gt;p</code>, <code>&lt;=p</code> or <code>&lt;p</code>,
where <code>p</code> is a PRISM language expression evaluating to a double in the range [0,1].
</p>
<p class='vspace'>The types of path property supported by PRISM and their semantics will be discussed shortly.
</p>
<div class='vspace'></div><h3>Nondeterminism</h3>
<p>For models that can exhibit nondeterministic behaviour (MDPs or PTAs), some additional clarifications are necessary. Whereas for fully probabilistic models such as DTMCs and CTMCs, probability measures over paths are well defined (see e.g. [<a class='wikilink' href='../Main/References.html#KSK76'>KSK76</a>] and [<a class='wikilink' href='../Main/References.html#BKH99'>BKH99</a>], respectively), for nondeterministic models a probability measure can only be feasibly defined once all nondeterminism has been removed.
</p>
<p class='vspace'>Hence, the actual meaning of the property <code>P bound [ pathprop ]</code> in these cases is:
"the probability that <code>pathprop</code> is satisfied by the paths from state <em>s</em>
meets the bound <code>bound</code> <em>for all possible resolutions of nondeterminism</em>".
This means that, properties using the <code><strong>P</strong></code> operator then effectively reason about the
<em>minimum</em> or <em>maximum</em> probability, over all possible resolutions of nondeterminism,
that a certain type of behaviour is observed.
This depends on the bound attached to the <code><strong>P</strong></code> operator:
a lower bound (<code>&gt;</code> or <code>&gt;=</code>) relates to minimum probabilities
and an upper bound (<code>&lt;</code> or <code>&lt;=</code>) to maximum probabilities.
</p>
<div class='vspace'></div><h3>Quantitative properties</h3>
<p>It is also very often useful to take a <em>quantitative</em> approach to probabilistic model checking, computing the actual probability that some behaviour of a model is observed,
rather than just verifying whether or not the probability is above or below a given bound.
Hence, PRISM allows the <code><strong>P</strong></code> operator to take the following form:
</p>
<div class='vspace'></div>
<div class='sourceblock ' id='sourceblock11'>
  <div class='sourceblocktext'><div class="prism"><span class="prismkeyword">P</span>=? [ <span class="prismident">pathprop</span> ]<br/>
</div></div>
  <div class='sourceblocklink'><a href='http://prismmodelchecker.localhost/manual/PropertySpecification/AllOnOnePage?action=sourceblock&amp;num=11' type='text/plain'>[&#036;[Get Code]]</a></div>
</div>

<p class='vspace'>These properties return a numerical rather than a Boolean value.
The <a class='wikilink' href='TheSOperator.html'>S</a> and <a class='wikilink' href='Reward-basedProperties.html'>R</a> operators, discussed later, can also be used in this way.
</p>
<p class='vspace'>As mentioned above, for nondeterministic models (MDPs or PTAs), either minimum or maximum probability values can be computed. Therefore, in this case, we have two possible types of property:
</p>
<div class='vspace'></div>
<div class='sourceblock ' id='sourceblock12'>
  <div class='sourceblocktext'><div class="prism"><span class="prismkeyword">Pmin</span>=? [ <span class="prismident">pathprop</span> ]<br/>
<span class="prismkeyword">Pmax</span>=? [ <span class="prismident">pathprop</span> ]<br/>
</div></div>
  <div class='sourceblocklink'><a href='http://prismmodelchecker.localhost/manual/PropertySpecification/AllOnOnePage?action=sourceblock&amp;num=12' type='text/plain'>[&#036;[Get Code]]</a></div>
</div>

<p class='vspace'>which return the minimum and maximum probabilities, respectively.
</p>
<p class='vspace'>It is also possible to specify to which state the probability returned by a quantitative property refers. This is covered in the later section on <a class='wikilink' href='Filters.html'>filters</a>.
</p>
<div class='vspace'></div><h3>Path properties</h3>
<p>PRISM supports a wide range of path properties that can be used with the <code><strong>P</strong></code> operator.
A path property is a formula that evaluates to either true or false for a single path in a model.
Here, we review some of the simpler properties that feature a single <em>temporal operator</em>,
as used for example in the logics PCTL and CSL. Later, we briefly describe how PRISM also supports more complex LTL-style path properties.
</p>
<p class='vspace'>The basic different types of path property that can be used inside the <code><strong>P</strong></code> operator are:
</p>
<div class='vspace'></div><ul><li><code><strong>X</strong></code> : "ne<strong>x</strong>t"
</li><li><code><strong>U</strong></code> : "<strong>u</strong>ntil"
</li><li><code><strong>F</strong></code> : "eventually" (sometimes called "<strong>f</strong>uture")
</li><li><code><strong>G</strong></code> : "always" (sometimes called "<strong>g</strong>lobally")
</li><li><code><strong>W</strong></code> : "<strong>w</strong>eak until"
</li><li><code><strong>R</strong></code> : "<strong>r</strong>elease"
</li></ul><p class='vspace'>In the following sections, we describe each of these <em>temporal operators</em>. We then discuss the (optional) use of time bounds with these operators. Finally, we also discuss LTL-style path properties.
</p>
<div class='vspace'></div><h3>"Next" path properties</h3>
<p>The property <code><strong>X</strong> prop</code> is true for a path if <code>prop</code> is true in its second state,
An example of this type of property, used inside a <code><strong>P</strong></code> operator, is:
</p>
<div class='vspace'></div>
<div class='sourceblock ' id='sourceblock13'>
  <div class='sourceblocktext'><div class="prism"><span class="prismkeyword">P</span>&lt;<span class="prismnum">0.01</span> [ <span class="prismkeyword">X</span> <span class="prismident">y</span>=<span class="prismnum">1</span> ]<br/>
</div></div>
  <div class='sourceblocklink'><a href='http://prismmodelchecker.localhost/manual/PropertySpecification/AllOnOnePage?action=sourceblock&amp;num=13' type='text/plain'>[&#036;[Get Code]]</a></div>
</div>

<p class='vspace'>which is true in a state if "the probability of the expression <code>y=1</code> being true in the next state is less than 0.01".
</p>
<div class='vspace'></div><h3>"Until" path properties</h3>
<p>The property <code>prop1 <strong>U</strong> prop2</code> is true for a path if
<code>prop2</code> is true in some state of the path and <code>prop1</code> is true in all preceding states.
A simple example of this would be:
</p>
<div class='vspace'></div>
<div class='sourceblock ' id='sourceblock14'>
  <div class='sourceblocktext'><div class="prism"><span class="prismkeyword">P</span>&gt;<span class="prismnum">0.5</span> [ <span class="prismident">z</span>&lt;<span class="prismnum">2</span> <span class="prismkeyword">U</span> <span class="prismident">z</span>=<span class="prismnum">2</span> ]<br/>
</div></div>
  <div class='sourceblocklink'><a href='http://prismmodelchecker.localhost/manual/PropertySpecification/AllOnOnePage?action=sourceblock&amp;num=14' type='text/plain'>[&#036;[Get Code]]</a></div>
</div>

<p class='vspace'>which is true in a state if "the probability that <code>z</code> is eventually equal to 2, and that <code>z</code> remains less than 2 up until that point, is greater than 0.5".
</p>
<div class='vspace'></div><h3>"Eventually" path properties</h3>
<p>The property <code><strong>F</strong> prop</code> is true for a path if <code>prop</code> eventually becomes true at some point along the path. The <code><strong>F</strong></code> operator is in fact a special case of the <code><strong>U</strong></code> operator (you will often see <code> <strong>F</strong> prop</code> written as <code><strong>true</strong> <strong>U</strong> prop</code>). A simple example is:
</p>
<div class='vspace'></div>
<div class='sourceblock ' id='sourceblock15'>
  <div class='sourceblocktext'><div class="prism"><span class="prismkeyword">P</span>&lt;<span class="prismnum">0.1</span> [ <span class="prismkeyword">F</span> <span class="prismident">z</span>&gt;<span class="prismnum">2</span> ]<br/>
</div></div>
  <div class='sourceblocklink'><a href='http://prismmodelchecker.localhost/manual/PropertySpecification/AllOnOnePage?action=sourceblock&amp;num=15' type='text/plain'>[&#036;[Get Code]]</a></div>
</div>

<p class='vspace'>which is true in a state if "the probability that <code>z</code> is eventually greater than 2is less than 0.1".
</p>
<div class='vspace'></div><h3>"Globally" path properties</h3>
<p>Whereas the <code><strong>F</strong></code> operator is used for "reachability" properties, <code><strong>G</strong></code> represents "invariance". The property <code><strong>G</strong> prop</code> is true of a path if <code>prop</code> remains true at all states along the path. Thus, for example:
</p>
<div class='vspace'></div>
<div class='sourceblock ' id='sourceblock16'>
  <div class='sourceblocktext'><div class="prism"><span class="prismkeyword">P</span>&gt;=<span class="prismnum">0.99</span> [ <span class="prismkeyword">G</span> <span class="prismident">z</span>&lt;<span class="prismnum">10</span> ]<br/>
</div></div>
  <div class='sourceblocklink'><a href='http://prismmodelchecker.localhost/manual/PropertySpecification/AllOnOnePage?action=sourceblock&amp;num=16' type='text/plain'>[&#036;[Get Code]]</a></div>
</div>

<p class='vspace'>states that, with probability at least 0.99, <code>z</code> never exceeds 10.
</p>
<div class='vspace'></div><h3>"Weak until" and "release" path properties</h3>
<p>Like <code><strong>F</strong></code> and <code><strong>G</strong></code>, the operators <code><strong>W</strong></code> and <code><strong>R</strong></code> are derivable from other temporal operators.
</p>
<p class='vspace'>Weak until (<code>a <strong>W</strong> b</code>), which is equivalent to <code>(a <strong>U</strong> b) | <strong>G</strong> a</code>, requires that <code>a</code> remains true until <code>b</code> becomes true, but does not require that <code>b</code> ever does becomes true (i.e. <code>a</code> remains true forever). For example, a weak form of the until example used above is:
</p>
<div class='vspace'></div>
<div class='sourceblock ' id='sourceblock17'>
  <div class='sourceblocktext'><div class="prism"><span class="prismkeyword">P</span>&gt;<span class="prismnum">0.5</span> [ <span class="prismident">z</span>&lt;<span class="prismnum">2</span> <span class="prismkeyword">U</span> <span class="prismident">z</span>=<span class="prismnum">2</span> ]<br/>
</div></div>
  <div class='sourceblocklink'><a href='http://prismmodelchecker.localhost/manual/PropertySpecification/AllOnOnePage?action=sourceblock&amp;num=17' type='text/plain'>[&#036;[Get Code]]</a></div>
</div>

<p class='vspace'>which states that, with probability greater than 0.5, either <code>z</code> is always less than 2, or it is less than 2 until the point where <code>z</code> is 2.
</p>
<p class='vspace'>Release (<code>a <strong>R</strong> b</code>),  which is equivalent to <code>!(!a U !b)</code>, informally means that <code>b</code> is true until <code>a</code> becomes true, or <code>b</code> is true forever.
</p>
<p class='vspace'><a name='bounded' id='bounded'></a>
</p><h3>"Bounded" variants of path properties</h3>
<p>All of the temporal operators given above, with the exception of <code><strong>X</strong></code>, have "bounded" variants, where an additional time bound is imposed on the property being satisfied.
The most common case is to use an upper time bound, i.e. of the form "<code>&lt;=t</code>" or "<code>&lt;t</code>", where <code>t</code> is a PRISM expression evaluating to a constant, non-negative value.
</p>
<p class='vspace'>For example, a bounded until property <code>prop1 <strong>U</strong>&lt;=t prop2</code>, is satisfied along a path if <code>prop2</code> becomes true within <code>t</code> steps and <code>prop1</code> is true in all states before that point.
A typical example of this would be:
</p>
<div class='vspace'></div>
<div class='sourceblock ' id='sourceblock18'>
  <div class='sourceblocktext'><div class="prism"><span class="prismkeyword">P</span>&gt;=<span class="prismnum">0.98</span> [ <span class="prismident">y</span>&lt;<span class="prismnum">4</span> <span class="prismkeyword">U</span>&lt;=<span class="prismnum">7</span> <span class="prismident">y</span>=<span class="prismnum">4</span> ]<br/>
</div></div>
  <div class='sourceblocklink'><a href='http://prismmodelchecker.localhost/manual/PropertySpecification/AllOnOnePage?action=sourceblock&amp;num=18' type='text/plain'>[&#036;[Get Code]]</a></div>
</div>

<p class='vspace'>which is true in a state if "the probability of <code>y</code> first exceeding 3 within 7 time units is greater than or equal to 0.98". Similarly:
</p>
<div class='vspace'></div>
<div class='sourceblock ' id='sourceblock19'>
  <div class='sourceblocktext'><div class="prism"><span class="prismkeyword">P</span>&gt;=<span class="prismnum">0.98</span> [ <span class="prismkeyword">F</span>&lt;=<span class="prismnum">7</span> <span class="prismident">y</span>=<span class="prismnum">4</span> ]<br/>
</div></div>
  <div class='sourceblocklink'><a href='http://prismmodelchecker.localhost/manual/PropertySpecification/AllOnOnePage?action=sourceblock&amp;num=19' type='text/plain'>[&#036;[Get Code]]</a></div>
</div>

<p class='vspace'>is true in a state if "the probability of <code>y</code> being equal to 4 within 7 time units is greater than or equal to 0.98" and:
</p>
<div class='vspace'></div>
<div class='sourceblock ' id='sourceblock20'>
  <div class='sourceblocktext'><div class="prism"><span class="prismkeyword">P</span>&gt;=<span class="prismnum">0.98</span> [ <span class="prismkeyword">G</span>&lt;=<span class="prismnum">7</span> <span class="prismident">y</span>=<span class="prismnum">4</span> ]<br/>
</div></div>
  <div class='sourceblocklink'><a href='http://prismmodelchecker.localhost/manual/PropertySpecification/AllOnOnePage?action=sourceblock&amp;num=20' type='text/plain'>[&#036;[Get Code]]</a></div>
</div>

<p class='vspace'>is true if the probability of <code>y</code> staying equal to 4 for 7 time units is at least 0.98.
</p>
<p class='vspace'>The time bound can be an arbitrary (constant) expression,
but note that you may need to bracket it,
as in the following example:
</p>
<div class='vspace'></div>
<div class='sourceblock ' id='sourceblock21'>
  <div class='sourceblocktext'><div class="prism"><span class="prismkeyword">P</span>&gt;=<span class="prismnum">0.98</span> [ <span class="prismkeyword">G</span>&lt;=(<span class="prismnum">2</span>*<span class="prismident">k</span>+<span class="prismnum">1</span>) <span class="prismident">y</span>=<span class="prismnum">4</span> ]<br/>
</div></div>
  <div class='sourceblocklink'><a href='http://prismmodelchecker.localhost/manual/PropertySpecification/AllOnOnePage?action=sourceblock&amp;num=21' type='text/plain'>[&#036;[Get Code]]</a></div>
</div>

<p class='vspace'>You can also use lower time-bounds (i.e. <code>&gt;=t</code> or <code>&gt;t</code>) and time intervals <code>[t1,t2]</code>, e.g.:
</p>
<div class='vspace'></div>
<div class='sourceblock ' id='sourceblock22'>
  <div class='sourceblocktext'><div class="prism"><span class="prismkeyword">P</span>&gt;=<span class="prismnum">0.98</span> [ <span class="prismkeyword">F</span>&gt;=<span class="prismnum">10</span> <span class="prismident">y</span>=<span class="prismnum">4</span> ]<br/>
<span class="prismkeyword">P</span>&gt;=<span class="prismnum">0.98</span> [ <span class="prismkeyword">F</span>[<span class="prismnum">10</span>,<span class="prismnum">20</span>] <span class="prismident">y</span>=<span class="prismnum">4</span> ]<br/>
</div></div>
  <div class='sourceblocklink'><a href='http://prismmodelchecker.localhost/manual/PropertySpecification/AllOnOnePage?action=sourceblock&amp;num=22' type='text/plain'>[&#036;[Get Code]]</a></div>
</div>

<p class='vspace'>which refer to the probability of <code>y</code> becoming equal to 4 after 10 or more time units, and after between 10 and 20 time-units respectively.
</p>
<p class='vspace'>For CTMCs, the time bounds can be any (non-negative) numerical values - they are not restricted to integers, as for DTMCs and MDPs.
For example:
</p>
<div class='vspace'></div>
<div class='sourceblock ' id='sourceblock23'>
  <div class='sourceblocktext'><div class="prism"><span class="prismkeyword">P</span>&gt;=<span class="prismnum">0.25</span> [ <span class="prismident">y</span>&lt;=<span class="prismnum">1</span> <span class="prismkeyword">U</span>&lt;=<span class="prismnum">6.5</span> <span class="prismident">y</span>&gt;<span class="prismnum">1</span> ]<br/>
</div></div>
  <div class='sourceblocklink'><a href='http://prismmodelchecker.localhost/manual/PropertySpecification/AllOnOnePage?action=sourceblock&amp;num=23' type='text/plain'>[&#036;[Get Code]]</a></div>
</div>

<p class='vspace'>means that the probability of <code>y</code> 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.
</p>
<div class='vspace'></div><h3>Transient probabilities</h3>
<p>We can also use the bounded <code><strong>F</strong></code> operator to refer to a single time instant, e.g.:
</p>
<div class='vspace'></div>
<div class='sourceblock ' id='sourceblock24'>
  <div class='sourceblocktext'><div class="prism"><span class="prismkeyword">P</span>=? [ <span class="prismkeyword">F</span>[<span class="prismnum">10</span>,<span class="prismnum">10</span>] <span class="prismident">y</span>=<span class="prismnum">6</span> ]<br/>
</div></div>
  <div class='sourceblocklink'><a href='http://prismmodelchecker.localhost/manual/PropertySpecification/AllOnOnePage?action=sourceblock&amp;num=24' type='text/plain'>[&#036;[Get Code]]</a></div>
</div>

<p class='vspace'>or, equivalently:
</p>
<div class='vspace'></div>
<div class='sourceblock ' id='sourceblock25'>
  <div class='sourceblocktext'><div class="prism"><span class="prismkeyword">P</span>=? [ <span class="prismkeyword">F</span>=<span class="prismnum">10</span> <span class="prismident">y</span>=<span class="prismnum">6</span> ]<br/>
</div></div>
  <div class='sourceblocklink'><a href='http://prismmodelchecker.localhost/manual/PropertySpecification/AllOnOnePage?action=sourceblock&amp;num=25' type='text/plain'>[&#036;[Get Code]]</a></div>
</div>

<p class='vspace'>both of which give the probability of <code>y</code> being 6 at time instant 10.
</p>
<p class='vspace'><a name='ltl' id='ltl'></a>
</p><h3>LTL-style path properties</h3>
<p>PRISM also supports probabilistic model checking of the temporal logic LTL (and, in fact, PCTL*). LTL provides a richer set of path properties for use with the <code><strong>P</strong></code> operator, by permitting temporal operators to be combined. Here are a few examples of properties expressible using this functionality:
</p>
<div class='vspace'></div>
<div class='sourceblock ' id='sourceblock26'>
  <div class='sourceblocktext'><div class="prism"><span class="prismkeyword">P</span>&gt;<span class="prismnum">0.99</span> [ <span class="prismkeyword">F</span> ( "<span class="prismident">request</span>" &amp; (<span class="prismkeyword">X</span> "<span class="prismident">ack</span>") ) ]<br/>
</div></div>
  <div class='sourceblocklink'><a href='http://prismmodelchecker.localhost/manual/PropertySpecification/AllOnOnePage?action=sourceblock&amp;num=26' type='text/plain'>[&#036;[Get Code]]</a></div>
</div>

<p class='vspace'>"with probability greater than 0.99, a request is eventually received, followed immediately by an acknowledgement"
</p>
<div class='vspace'></div>
<div class='sourceblock ' id='sourceblock27'>
  <div class='sourceblocktext'><div class="prism"><span class="prismkeyword">P</span>&gt;=<span class="prismnum">1</span> [ <span class="prismkeyword">G</span> <span class="prismkeyword">F</span> "<span class="prismident">send</span>" ]<br/>
</div></div>
  <div class='sourceblocklink'><a href='http://prismmodelchecker.localhost/manual/PropertySpecification/AllOnOnePage?action=sourceblock&amp;num=27' type='text/plain'>[&#036;[Get Code]]</a></div>
</div>

<p class='vspace'>"a message is sent infinitely often with probability 1"
</p>
<div class='vspace'></div>
<div class='sourceblock ' id='sourceblock28'>
  <div class='sourceblocktext'><div class="prism"><span class="prismkeyword">P</span>=? [ <span class="prismkeyword">F</span> <span class="prismkeyword">G</span> ("<span class="prismident">error</span>" &amp; !"<span class="prismident">repair</span>") ]<br/>
</div></div>
  <div class='sourceblocklink'><a href='http://prismmodelchecker.localhost/manual/PropertySpecification/AllOnOnePage?action=sourceblock&amp;num=28' type='text/plain'>[&#036;[Get Code]]</a></div>
</div>

<p class='vspace'>"the probability of an error occurring that is never repaired
</p>
<p class='vspace'>Note that logical operators have precedence over temporal ones, so you will often need to include parentheses when using logical operators, e.g.:
</p>
<div class='vspace'></div>
<div class='sourceblock ' id='sourceblock29'>
  <div class='sourceblocktext'><div class="prism"><span class="prismkeyword">P</span>=? [ (<span class="prismkeyword">F</span> "<span class="prismident">error1</span>") &amp; (<span class="prismkeyword">F</span> "<span class="prismident">error2</span>") ]<br/>
</div></div>
  <div class='sourceblocklink'><a href='http://prismmodelchecker.localhost/manual/PropertySpecification/AllOnOnePage?action=sourceblock&amp;num=29' type='text/plain'>[&#036;[Get Code]]</a></div>
</div>

<p class='vspace'>For temporal operators, unary operators (such as <code><strong>F</strong></code>, <code><strong>G</strong></code> and <code><strong>X</strong></code>) have precedence over binary ones (such as <code><strong>U</strong></code>). Unary operators can be nested, without parentheses, but binary ones cannot.
</p>
<p class='vspace'>So, these are allowed:
</p>
<div class='vspace'></div>
<div class='sourceblock ' id='sourceblock30'>
  <div class='sourceblocktext'><div class="prism"><span class="prismkeyword">P</span>=? [ <span class="prismkeyword">F</span> <span class="prismkeyword">X</span> <span class="prismkeyword">X</span> <span class="prismkeyword">X</span> "<span class="prismident">a</span>" ]<br/>
<span class="prismkeyword">P</span>=? [ "<span class="prismident">a</span>" <span class="prismkeyword">U</span> <span class="prismkeyword">X</span> <span class="prismkeyword">X</span> <span class="prismkeyword">X</span> "<span class="prismident">error</span>" ]<br/>
<span class="prismkeyword">P</span>=? [ ("<span class="prismident">a</span>" <span class="prismkeyword">U</span> "<span class="prismident">b</span>") <span class="prismkeyword">U</span> "<span class="prismident">c</span>" "<span class="prismident">error</span>" ]<br/>
</div></div>
  <div class='sourceblocklink'><a href='http://prismmodelchecker.localhost/manual/PropertySpecification/AllOnOnePage?action=sourceblock&amp;num=30' type='text/plain'>[&#036;[Get Code]]</a></div>
</div>

<p class='vspace'>but this is not:
</p>
<div class='vspace'></div>
<div class='sourceblock ' id='sourceblock31'>
  <div class='sourceblocktext'><div class="prism"><span class="prismkeyword">P</span>=? [ "<span class="prismident">a</span>" <span class="prismkeyword">U</span> "<span class="prismident">b</span>" <span class="prismkeyword">U</span> "<span class="prismident">c</span>" "<span class="prismident">error</span>" ]<br/>
</div></div>
  <div class='sourceblocklink'><a href='http://prismmodelchecker.localhost/manual/PropertySpecification/AllOnOnePage?action=sourceblock&amp;num=31' type='text/plain'>[&#036;[Get Code]]</a></div>
</div>

<hr />
<h1>The S Operator</h1>
<p>The <code><strong>S</strong></code> operator is used to reason about the <em>steady-state</em> behaviour of a model,
i.e. its behaviour in the <em>long-run</em> or <em>equilibrium</em>.
Although this could in principle relate to all three model types,
PRISM currently only provides support for DTMCs and CTMCs.
The definition of steady-state (long-run) probabilities for finite DTMCS and CTMCs is well defined (see e.g. [<a class='wikilink' href='../Main/References.html#Ste94'>Ste94</a>]).
Informally, the property:
</p>
<div class='vspace'></div>
<div class='sourceblock ' id='sourceblock32'>
  <div class='sourceblocktext'><div class="prism"><span class="prismkeyword">S</span> <span class="prismident">bound</span> [ <span class="prismident">prop</span> ]<br/>
</div></div>
  <div class='sourceblocklink'><a href='http://prismmodelchecker.localhost/manual/PropertySpecification/AllOnOnePage?action=sourceblock&amp;num=32' type='text/plain'>[&#036;[Get Code]]</a></div>
</div>

<p class='vspace'>is true in a state <em>s</em> of a DTMC or CTMC if
"starting from <em>s</em>, the steady-state (long-run) probability of being in a state which satisfies the (Boolean-valued) PRISM property <code>prop</code>, meets the bound <code>bound</code>".
A typical example of this type of property would be:
</p>
<div class='vspace'></div>
<div class='sourceblock ' id='sourceblock33'>
  <div class='sourceblocktext'><div class="prism"><span class="prismkeyword">S</span>&lt;<span class="prismnum">0.05</span> [ <span class="prismident">queue_size</span> / <span class="prismident">max_size</span> &gt; <span class="prismnum">0.75</span> ]<br/>
</div></div>
  <div class='sourceblocklink'><a href='http://prismmodelchecker.localhost/manual/PropertySpecification/AllOnOnePage?action=sourceblock&amp;num=33' type='text/plain'>[&#036;[Get Code]]</a></div>
</div>

<p class='vspace'>which means: "the long-run probability of the queue being more than 75% full is less than 0.05".
</p>
<p class='vspace'>Like the <code><strong>P</strong></code> <a class='wikilink' href='ThePOperator.html'>operator</a>, the <code><strong>S</strong></code> operator can be used in a <em>quantitative</em> form, which returns the actual probability value, e.g.:
</p>
<div class='vspace'></div>
<div class='sourceblock ' id='sourceblock34'>
  <div class='sourceblocktext'><div class="prism"><span class="prismkeyword">S</span>=? [ <span class="prismident">queue_size</span> / <span class="prismident">max_size</span> &gt; <span class="prismnum">0.75</span> ]<br/>
</div></div>
  <div class='sourceblocklink'><a href='http://prismmodelchecker.localhost/manual/PropertySpecification/AllOnOnePage?action=sourceblock&amp;num=34' type='text/plain'>[&#036;[Get Code]]</a></div>
</div>

<p class='vspace'>and can be further customised with the use of <a class='wikilink' href='Filters.html'>filters</a>.
</p><hr />
<h1>Reward-based Properties</h1>
<p>PRISM models can be augmented with information about <a class='wikilink' href='../ThePRISMLanguage/CostsAndRewards.html'>rewards</a> (or, equivalently, costs).
The tool can analyse properties which relate to the <em>expected values</em> of these rewards.
This is achieved using the <code><strong>R</strong></code> operator, which works in a similar fashion to the
<code><strong>P</strong></code> and <code><strong>S</strong></code> operators, and can be used either in a Boolean-valued query, e.g.:
</p>
<div class='vspace'></div>
<div class='sourceblock ' id='sourceblock35'>
  <div class='sourceblocktext'><div class="prism"><span class="prismkeyword">R</span> <span class="prismident">bound</span> [ <span class="prismident">rewardprop</span> ]<br/>
</div></div>
  <div class='sourceblocklink'><a href='http://prismmodelchecker.localhost/manual/PropertySpecification/AllOnOnePage?action=sourceblock&amp;num=35' type='text/plain'>[&#036;[Get Code]]</a></div>
</div>

<p class='vspace'>where <code>bound</code> takes the form <code>&lt;r</code>, <code>&lt;=r</code>, <code>&gt;r</code> or <code>&gt;=r</code> for an expression <code>r</code> evaluating to a non-negative double,
or a real-valued query, e.g.:
</p>
<div class='vspace'></div>
<div class='sourceblock ' id='sourceblock36'>
  <div class='sourceblocktext'><div class="prism"><span class="prismkeyword">R</span> <span class="prismident">query</span> [ <span class="prismident">rewardprop</span> ]<br/>
</div></div>
  <div class='sourceblocklink'><a href='http://prismmodelchecker.localhost/manual/PropertySpecification/AllOnOnePage?action=sourceblock&amp;num=36' type='text/plain'>[&#036;[Get Code]]</a></div>
</div>

<p class='vspace'>where <code>query</code> is <code>=?</code>, <code>min=?</code> or <code>max=?</code>.
In the latter case, <a class='wikilink' href='Filters.html'>filters</a> can be used, as for the <code><strong>P</strong></code> and <code><strong>S</strong></code> operators.
</p>
<p class='vspace'>Informally, "<code><strong>R</strong> bound [ rewardprop ]</code>" is true in a state of a model if
"the expected reward associated with <code>rewardprop</code> of the model when starting from that state''
meets the bound <code>bound</code> and "<code><strong>R</strong> query [ rewardprop ]</code>"  returns the actual expected reward value.
</p>
<p class='vspace'>There are various different types of reward properties:
</p>
<div class='vspace'></div><ul><li>"reachability reward": <code><strong>F</strong> prop</code>
</li><li>"cumulative reward" : <code><strong>C</strong>&lt;=t</code>
</li><li>"total reward" : <code><strong>C</strong></code>
</li><li>"instantaneous reward" : <code><strong>I</strong>=t</code>
</li><li>"steady-state reward" : <code><strong>S</strong></code>.
</li></ul><p class='vspace'>Below, we consider each of these cases in turn.
The descriptions here are kept relatively informal.
Precise definitions for most of these can be found in, for example,
[<a class='wikilink' href='../Main/References.html#KNP07a'>KNP07a</a>] (for DTMCs and CTMCs) or [<a class='wikilink' href='../Main/References.html#FKNP11'>FKNP11</a>] (for MDPs).
</p>
<div class='vspace'></div><h3>"Reachability reward" properties</h3>
<p>"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 <em>rate</em> at which rewards are accumulated in that state,
i.e. if <em>t</em> time units are spent in a state with state reward <em>r</em>,
the reward accumulated in that state is <em>r</em> x <em>t</em>.
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.
</p>
<p class='vspace'>The reward property "<code>F prop</code>" corresponds to the reward cumulated along a path
until a state satisfying property <code>prop</code> is reached,
where rewards are cumulated as described above.
State rewards for the <code>prop</code>-satisfying state reached are not included in the cumulated value.
In the case where the probability of reaching a state satisfying <code>prop</code> is less than 1, the reward is equal to infinity.
</p>
<p class='vspace'>A common application of this type of property is the case when the rewards associated with the model correspond to time.
One can then state, for example:
</p>
<div class='vspace'></div>
<div class='sourceblock ' id='sourceblock37'>
  <div class='sourceblocktext'><div class="prism"><span class="prismkeyword">R</span>&lt;=<span class="prismnum">9.5</span> [ <span class="prismkeyword">F</span> <span class="prismident">z</span>=<span class="prismnum">2</span> ]<br/>
</div></div>
  <div class='sourceblocklink'><a href='http://prismmodelchecker.localhost/manual/PropertySpecification/AllOnOnePage?action=sourceblock&amp;num=37' type='text/plain'>[&#036;[Get Code]]</a></div>
</div>

<p class='vspace'>which is true in a state <em>s</em> if "the expected time taken to reach, from <em>s</em>, a state where <code>z</code> equals 2 is less than or equal to 9.5".
</p>
<div class='vspace'></div><h3>"Cumulative reward" properties</h3>
<p>"Cumulative reward" properties also associate a reward with each path of a model,
but only up to a given time bound.
The property <code>C&lt;=t</code> corresponds to the reward cumulated along a path
until <code>t</code> time units have elapsed.
For DTMCs and MDPs, the bound <code>t</code> must evaluate to an integer;
for CTMCs, it can evaluate to double.
State and transition rewards along a path are cumulated exactly as described in the previous section.
</p>
<p class='vspace'>A typical application of this type of property is the following.
Consider a model of a disk-drive controller which includes a queue of incoming disk requests.
If we assign a reward of 1 to each transition of the model
corresponding to the situation where an incoming request is lost because the queue is full,
then the property:
</p>
<div class='vspace'></div>
<div class='sourceblock ' id='sourceblock38'>
  <div class='sourceblocktext'><div class="prism"><span class="prismkeyword">R</span>=? [ <span class="prismkeyword">C</span>&lt;=<span class="prismnum">15.5</span> ]<br/>
</div></div>
  <div class='sourceblocklink'><a href='http://prismmodelchecker.localhost/manual/PropertySpecification/AllOnOnePage?action=sourceblock&amp;num=38' type='text/plain'>[&#036;[Get Code]]</a></div>
</div>

<p class='vspace'>would return, for a given state of the model,
"the expected number of lost requests within 15.5 time units of operation".
</p>
<p class='vspace'><a name='total' id='total'></a>
</p><h3>"Total reward" properties</h3>
<p>"Total reward" properties refer to the accumulation of state and transition rewards
in the same way as for "reachability reward" and "cumulative reward" properties,
but the rewards is accumulated indefinitely,
i.e. the total reward accumulated along the whole (infinite) path.
Note that this means that, unless a path ends up remaining forever in states with zero reward,
the total reward will be infinite.
</p>
<p class='vspace'>Re-using the reward structure in the previous example,
</p>
<div class='vspace'></div>
<div class='sourceblock ' id='sourceblock39'>
  <div class='sourceblocktext'><div class="prism"><span class="prismkeyword">R</span>=? [ <span class="prismkeyword">C</span>&lt;=<span class="prismnum">15.5</span> ]<br/>
</div></div>
  <div class='sourceblocklink'><a href='http://prismmodelchecker.localhost/manual/PropertySpecification/AllOnOnePage?action=sourceblock&amp;num=39' type='text/plain'>[&#036;[Get Code]]</a></div>
</div>

<p class='vspace'>returns "the expected total number of lost requests".
</p>
<div class='vspace'></div><h3>"Instantaneous reward" properties</h3>
<p>"Instantaneous reward" properties refer to the reward of a model at a particular instant in time.
The reward property <code>I=t</code> associates with a path the reward in the state
of that path when exactly <code>t</code> time units have elapsed.
For DTMCs and MDPs, the bound <code>t</code> must evaluate to an integer;
for CTMCs, it can evaluate to double.
</p>
<p class='vspace'>Returning to our example from the previous section of a model for a disk-request queue in a disk-drive controller,
consider the case where the rewards assigned to each state of the model give the current size of the queue in that state.
Then, the following property:
</p>
<div class='vspace'></div>
<div class='sourceblock ' id='sourceblock40'>
  <div class='sourceblocktext'><div class="prism"><span class="prismkeyword">R</span>&lt;<span class="prismnum">4.4</span> [ <span class="prismkeyword">I</span>=<span class="prismnum">100</span> ]<br/>
</div></div>
  <div class='sourceblocklink'><a href='http://prismmodelchecker.localhost/manual/PropertySpecification/AllOnOnePage?action=sourceblock&amp;num=40' type='text/plain'>[&#036;[Get Code]]</a></div>
</div>

<p class='vspace'>would be true in a state <em>s</em> of the model if
"starting from <em>s</em>, the expected queue size exactly 100 time units later is less than 4.4".
Note that, for this type of reward property, state rewards for CTMCs do not have to refer to rates;
they can refer to any instantaneous measure of interest for a state.
</p>
<div class='vspace'></div><h3>"Steady-state reward" properties</h3>
<p>Unlike the previous three types of property,
"steady-state reward" properties relate not to paths, but rather to the reward in the long-run.
A typical application of this type of property would be, in the case where
the rewards associated with the model correspond to power consumption, the property:
</p>
<div class='vspace'></div>
<div class='sourceblock ' id='sourceblock41'>
  <div class='sourceblocktext'><div class="prism"><span class="prismkeyword">R</span>&lt;=<span class="prismnum">0.7</span> [ <span class="prismkeyword">S</span> ]<br/>
</div></div>
  <div class='sourceblocklink'><a href='http://prismmodelchecker.localhost/manual/PropertySpecification/AllOnOnePage?action=sourceblock&amp;num=41' type='text/plain'>[&#036;[Get Code]]</a></div>
</div>

<p class='vspace'>which is true in a state <em>s</em> if "starting from <em>s</em>, the long-run average power consumption is less than 0.7".
</p>
<div class='vspace'></div><h3>Which reward structure?</h3>
<p>In the case where a PRISM model has multiple <a class='wikilink' href='../ThePRISMLanguage/CostsAndRewards.html'>reward structures</a> you may need to specify which reward structure your property refers to. This is done by placing the information in braces (<code>{}</code>) after the <code>R</code> operator. You can do so either using the name assigned to a reward structure (if any) or using the index (where <code>1</code> means the first rewards structure in the PRISM model file, <code>2</code> the second, etc.). Examples are:
</p>
<div class='vspace'></div>
<div class='sourceblock ' id='sourceblock42'>
  <div class='sourceblocktext'><div class="prism"><span class="prismkeyword">R</span>{"<span class="prismident">num_failures</span>"}=? [ <span class="prismkeyword">C</span>&lt;=<span class="prismnum">10.0</span> ]<br/>
<span class="prismkeyword">R</span>{"<span class="prismident">time</span>"}=? [ <span class="prismkeyword">F</span> <span class="prismident">step</span>=<span class="prismident">final</span> ]<br/>
<span class="prismkeyword">R</span>{<span class="prismnum">2</span>}=? [ <span class="prismkeyword">F</span> <span class="prismident">step</span>=<span class="prismident">final</span> ]<br/>
</div></div>
  <div class='sourceblocklink'><a href='http://prismmodelchecker.localhost/manual/PropertySpecification/AllOnOnePage?action=sourceblock&amp;num=42' type='text/plain'>[&#036;[Get Code]]</a></div>
</div>

<p class='vspace'>Note that when using an index to specify the reward structure, you can actually put any expression that evaluates to an integer. This allows you to, for example, write a property of the form <code>R{c}=?[...]</code> where <code>c</code> is an undefined integer constant. You can then vary the value of <code>c</code> in an experiment and compute values for several different reward structures at once.
</p>
<p class='vspace'>If you don't specify a reward structure to the <code>R</code> operator, by default, the first one in the model file is used.
</p>
<div class='vspace'></div><h3>Availability</h3>
<p>There are currently a few restrictions on the model checking <a class='wikilink' href='../ConfiguringPRISM/ComputationEngines.html'>engines</a> that can be used for some reward properties. The following table summarises the currently availability, where S, M and H denote the "sparse", "MTBDD", "hybrid" and "explicit" engines, respectively, for DTMCs, CTMCs and MDPs. For PTAs, support for rewards is currently quite restrictive; see the later section on "<a class='wikilink' href='PTAProperties.html'>PTA properties</a>" for details.
</p>
<div class='vspace'></div>
<table border='1' cellpadding='5' ><tr ><td >&nbsp;</td><td  align='center'><code><strong>F</strong></code></td><td  align='center'><code><strong>C</strong>&lt;=t</code></td><td  align='center'><code><strong>C</strong></code></td><td  align='left'><code><strong>I</strong>=t</code></td><td  align='right'><code><strong>S</strong></code></td></tr>
<tr ><td  align='center'><strong>DTMCs</strong></td><td  align='center'>SMHE</td><td  align='center'>SMHE</td><td  align='center'>SMHE</td><td  align='center'>SMHE</td><td  align='right'>SMH-</td></tr>
<tr ><td  align='center'><strong>CTMCs</strong></td><td  align='center'>SMHE</td><td  align='center'>SMHE</td><td  align='center'>----</td><td  align='center'>SMHE</td><td  align='right'>SMH-</td></tr>
<tr ><td  align='center'><strong>MDPs</strong></td><td  align='center'>SM-E</td><td  align='center'>S--E</td><td  align='center'>----</td><td  align='center'>SM--</td><td  align='right'>----</td></tr>
</table><hr />
<h1>Non-Probabilistic Properties</h1>
<p>PRISM also supports most operators from the temporal logic CTL [<a class='wikilink' href='../Main/References.html#CE81'>CE81</a>], of which the probabilistic logics PCTL and CSL are an extension. CTL uses the <code><strong>A</strong></code> (for all) and <code><strong>E</strong></code> (there exists) operators, instead of the probabilistic <code><strong>P</strong></code> operator, to ask whether all (or some) paths from a state satisfy a particular path formula.
</p>
<p class='vspace'>For example:
</p>
<div class='vspace'></div>
<div class='sourceblock ' id='sourceblock43'>
  <div class='sourceblocktext'><div class="prism"><span class="prismkeyword">E</span> [ <span class="prismkeyword">F</span> "<span class="prismident">goal</span>" ]<br/>
<span class="prismkeyword">A</span> [ <span class="prismkeyword">F</span> "<span class="prismident">goal</span>" ]<br/>
</div></div>
  <div class='sourceblocklink'><a href='http://prismmodelchecker.localhost/manual/PropertySpecification/AllOnOnePage?action=sourceblock&amp;num=43' type='text/plain'>[&#036;[Get Code]]</a></div>
</div>

<p class='vspace'>mean "there exists a path that reaches a state labelled with <code>goal</code>"
and "all paths reach a state labelled with <code>goal</code>", respectively.
</p>
<p class='vspace'>Similarly:
</p>
<div class='vspace'></div>
<div class='sourceblock ' id='sourceblock44'>
  <div class='sourceblocktext'><div class="prism"><span class="prismkeyword">E</span> [ <span class="prismkeyword">G</span> "<span class="prismident">inv</span>" ]<br/>
<span class="prismkeyword">A</span> [ <span class="prismkeyword">G</span> "<span class="prismident">inv</span>" ]<br/>
</div></div>
  <div class='sourceblocklink'><a href='http://prismmodelchecker.localhost/manual/PropertySpecification/AllOnOnePage?action=sourceblock&amp;num=44' type='text/plain'>[&#036;[Get Code]]</a></div>
</div>

<p class='vspace'>state that some path (or all paths) satisfy <code><strong>G</strong> "inv"</code>, meaning that label <code>"inv"</code> holds in every state along the path.
</p>
<div class='vspace'></div><h3>Counterexamples and Witnesses</h3>
<p>If you check a property of the form <code>A [ G "inv" ]</code> and it is false, PRISM will generate a counterexample in the form of a path that reaches a state where <code>"inv"</code> is not true. This is displayed either in the simulator (from the GUI) or at the command-line. Similarly, if you check <code>E [ F "goal" ]</code> and the result is true, a witness (a path reaching a <code>"goal"</code> state) will be generated.
</p><hr />
<h1>Syntax And Semantics</h1>
<h3>Syntax</h3>
<p>The syntax of the PRISM property specification language subsumes various probabilistic temporal logics, including PCTL, CSL, (probabilistic) LTL, PCTL* and CTL. Informally, the syntax can be summarised as follows: a property can be any valid, well-typed PRISM <a class='wikilink' href='../ThePRISMLanguage/Expressions.html'>expression</a>, which (optionally) also includes the probabilistic operators discussed previously (<code><strong>P</strong></code>, <code><strong>S</strong></code> and <code><strong>R</strong></code>) and the non-probabilistic (CTL) ones <code><strong>A</strong></code> and <code><strong>E</strong></code>). This mean that any of the following operators can be used:
</p>
<div class='vspace'></div><ul><li><code>-</code> (unary minus)
</li><li><code>*</code>, <code>/</code> (multiplication, division)
</li><li><code>+</code>, <code>-</code> (addition, subtraction)
</li><li><code>&lt;</code>, <code>&lt;=</code>, <code>&gt;=</code>, <code>&gt;</code> (relational operators)
</li><li><code>=</code>, <code>!=</code> (equality operators)
</li><li><code>!</code> (negation)
</li><li><code>&amp;</code> (conjunction)
</li><li><code>|</code> (disjunction)
</li><li><code>&lt;=&gt;</code> (if-and-only-if)
</li><li><code>=&gt;</code> (implication)
</li><li><code>?</code> (condition evaluation: <code>condition ? a : b</code> means "if <code>condition</code> is true then <code>a</code> else <code>b</code>")
</li><li><code><strong>P</strong></code> (probabilistic operator)
</li><li><code><strong>S</strong></code> (steady-state operator)
</li><li><code><strong>R</strong></code> (reward operator)
</li><li><code><strong>A</strong></code> (for-all operator)
</li><li><code><strong>E</strong></code> (there-exists operator)
</li></ul><p class='vspace'>This allows you to write any property expressible in logics such as PCTL and CSL. For example, CSL allows you to nest <code><strong>P</strong></code> and <code><strong>S</strong></code> operators:
</p>
<div class='vspace'></div>
<div class='sourceblock ' id='sourceblock45'>
  <div class='sourceblocktext'><div class="prism"><span class="prismkeyword">P</span>=? [ <span class="prismkeyword">F</span>&gt;<span class="prismnum">2</span> <span class="prismkeyword">S</span>&gt;<span class="prismnum">0.9</span>[ <span class="prismident">num_servers</span> &gt;= <span class="prismnum">5</span> ] ]<br/>
</div></div>
  <div class='sourceblocklink'><a href='http://prismmodelchecker.localhost/manual/PropertySpecification/AllOnOnePage?action=sourceblock&amp;num=45' type='text/plain'>[&#036;[Get Code]]</a></div>
</div>

<p class='vspace'>"the probability of it taking more than 2 hours to get to a state from which the long-run probability of at least 5 servers being operational is &gt;0.9"
</p>
<p class='vspace'>You can also express various arithmetic expressions such as:
</p>
<div class='vspace'></div>
<div class='sourceblock ' id='sourceblock46'>
  <div class='sourceblocktext'><div class="prism"><span class="prismnum">1</span> - <span class="prismkeyword">P</span>=? [ <span class="prismkeyword">F</span>[<span class="prismnum">3600</span>,<span class="prismnum">7200</span>] <span class="prismident">oper</span> ]<br/>
</div></div>
  <div class='sourceblocklink'><a href='http://prismmodelchecker.localhost/manual/PropertySpecification/AllOnOnePage?action=sourceblock&amp;num=46' type='text/plain'>[&#036;[Get Code]]</a></div>
</div>

<p class='vspace'>"the probability that the system is <strong>not</strong> operational at any point during the second hour of operation"
</p>
<div class='vspace'></div>
<div class='sourceblock ' id='sourceblock47'>
  <div class='sourceblocktext'><div class="prism"><span class="prismkeyword">R</span>{"<span class="prismident">oper</span>"}=? [ <span class="prismkeyword">C</span>&lt;=<span class="prismident">t</span> ] / <span class="prismident">t</span><br/>
</div></div>
  <div class='sourceblocklink'><a href='http://prismmodelchecker.localhost/manual/PropertySpecification/AllOnOnePage?action=sourceblock&amp;num=47' type='text/plain'>[&#036;[Get Code]]</a></div>
</div>

<p class='vspace'>"the expected fraction of time that the system is available (i.e. the expected interval availability) in the time interval [0, t]"
</p>
<div class='vspace'></div>
<div class='sourceblock ' id='sourceblock48'>
  <div class='sourceblocktext'><div class="prism"><span class="prismkeyword">P</span>=? [ <span class="prismkeyword">F</span> <span class="prismident">fail_A</span> ] / <span class="prismkeyword">P</span>=? [ <span class="prismkeyword">F</span> <span class="prismident">any_fail</span> ]<br/>
</div></div>
  <div class='sourceblocklink'><a href='http://prismmodelchecker.localhost/manual/PropertySpecification/AllOnOnePage?action=sourceblock&amp;num=48' type='text/plain'>[&#036;[Get Code]]</a></div>
</div>

<p class='vspace'>"the (conditional) probability that component A eventually fails, given
that at least one component fails"
</p>
<div class='vspace'></div><h3>Semantics</h3>
<p>We omit a formal presentation of the semantics of the PRISM property language. The semantics of the probabilistic temporal logics that the language incorporates can be found from a variety of sources. See for example the pointers given in the <a class='urllink' href='http://www.prismmodelchecker.org/about.php'>About</a> and <a class='urllink' href='http://www.prismmodelchecker.org/doc/'>Documentation</a> sections of the PRISM website.
</p>
<p class='vspace'>It is worth, however, clarifying a few points specific to PRISM. A property is evaluated with respect to a particular state of a model. Depending on the type of the property, this value may either be a Boolean, an integer or a double. When performing model checking, PRISM usually has to actually compute the value for <em>all</em> states of the model but, for clarity, will by default report just a single value. Typically, this is the value for the (single) initial state of the model. For example, this:
</p>
<div class='vspace'></div>
<div class='sourceblock ' id='sourceblock49'>
  <div class='sourceblocktext'><div class="prism"><span class="prismkeyword">P</span>=? [ <span class="prismkeyword">F</span> "<span class="prismident">error</span>" ]<br/>
</div></div>
  <div class='sourceblocklink'><a href='http://prismmodelchecker.localhost/manual/PropertySpecification/AllOnOnePage?action=sourceblock&amp;num=49' type='text/plain'>[&#036;[Get Code]]</a></div>
</div>

<p class='vspace'>will report the probability, from the initial state of the model, of reaching an "error" state.
This:
</p>
<div class='vspace'></div>
<div class='sourceblock ' id='sourceblock50'>
  <div class='sourceblocktext'><div class="prism"><span class="prismkeyword">P</span>&gt;<span class="prismnum">0.5</span> [ <span class="prismkeyword">F</span> "<span class="prismident">error</span>" ]<br/>
</div></div>
  <div class='sourceblocklink'><a href='http://prismmodelchecker.localhost/manual/PropertySpecification/AllOnOnePage?action=sourceblock&amp;num=50' type='text/plain'>[&#036;[Get Code]]</a></div>
</div>

<p class='vspace'>will return <code>true</code> if and only if the probability, from the initial state, is greater than 0.5.
</p>
<p class='vspace'><strong>Note:</strong> This is contrast to older versions of PRISM, which treated numerical and Boolean-valued properties differently in this respect.
</p>
<p class='vspace'>For models with <a class='wikilink' href='../ThePRISMLanguage/MultipleInitialStates.html'>multiple initial states</a>, we need to adapt these definitions slightly. In this case, the two properties above will yield, respectively:
</p>
<div class='vspace'></div><ul><li>the range of values (over all initial states) of the probability of reaching "error"
<div class='vspace'></div></li><li><code>true</code> if and only if the probability is greater than 0.5 from <em>all</em> initial states.
</li></ul><p class='vspace'>You can also ask PRISM to return different values using <a class='wikilink' href='Filters.html'>filters</a>,
which are described in the next section.
</p><hr />
<h1>Filters</h1>
<p>As discussed above, when reporting the result of model checking a property, PRISM will by default return the value for the (single) initial state of the model. However, since PRISM in fact usually has to compute values for <em>all</em> states simultaneously, you can customise PRISM properties to obtain different results. This is done using <em>filters</em>.
</p>
<p class='vspace'>Filters are created using the <code>filter</code> keyword. They take the following form:
</p>
<div class='vspace'></div>
<div class='sourceblock ' id='sourceblock51'>
  <div class='sourceblocktext'><div class="prism"><span class="prismkeyword">filter</span>(<span class="prismident">op</span>, <span class="prismident">prop</span>, <span class="prismident">states</span>)<br/>
</div></div>
  <div class='sourceblocklink'><a href='http://prismmodelchecker.localhost/manual/PropertySpecification/AllOnOnePage?action=sourceblock&amp;num=51' type='text/plain'>[&#036;[Get Code]]</a></div>
</div>

<p class='vspace'>where <code>op</code> is the filter <em>operator</em> (see below), <code>prop</code> is any PRISM property and <code>states</code> is a Boolean-valued expression identifying a set of states over which to apply the filter.
</p>
<p class='vspace'>In fact, the <code>states</code> argument is optional; if omitted, the filter is applied over all states. So, the following properties are equivalent:
</p>
<div class='vspace'></div>
<div class='sourceblock ' id='sourceblock52'>
  <div class='sourceblocktext'><div class="prism"><span class="prismkeyword">filter</span>(<span class="prismident">op</span>, <span class="prismident">prop</span>)<br/>
<span class="prismkeyword">filter</span>(<span class="prismident">op</span>, <span class="prismident">prop</span>, <span class="prismkeyword">true</span>)<br/>
</div></div>
  <div class='sourceblocklink'><a href='http://prismmodelchecker.localhost/manual/PropertySpecification/AllOnOnePage?action=sourceblock&amp;num=52' type='text/plain'>[&#036;[Get Code]]</a></div>
</div>

<p class='vspace'>Here's a simple example of a filter:
</p>
<div class='vspace'></div>
<div class='sourceblock ' id='sourceblock53'>
  <div class='sourceblocktext'><div class="prism"><span class="prismkeyword">filter</span>(<span class="prismkeyword">max</span>, <span class="prismkeyword">P</span>=? [ <span class="prismkeyword">F</span> "<span class="prismident">error</span>" ], <span class="prismident">x</span>=<span class="prismnum">0</span>)<br/>
</div></div>
  <div class='sourceblocklink'><a href='http://prismmodelchecker.localhost/manual/PropertySpecification/AllOnOnePage?action=sourceblock&amp;num=53' type='text/plain'>[&#036;[Get Code]]</a></div>
</div>

<p class='vspace'>This gives the <em>maximum</em> value, starting from any state satisfying <code>x=0</code>, of the probability of reaching an "error" state.
</p>
<p class='vspace'>Here's another simple example,
which checks whether, <em>starting from any reachable state</em>,
we eventually reach a "done" state with probability 1.
</p>
<div class='vspace'></div>
<div class='sourceblock ' id='sourceblock54'>
  <div class='sourceblocktext'><div class="prism"><span class="prismkeyword">filter</span>(<span class="prismident">forall</span>, <span class="prismkeyword">P</span>&gt;=<span class="prismnum">1</span> [ <span class="prismkeyword">F</span> "<span class="prismident">done</span>" ])<br/>
</div></div>
  <div class='sourceblocklink'><a href='http://prismmodelchecker.localhost/manual/PropertySpecification/AllOnOnePage?action=sourceblock&amp;num=54' type='text/plain'>[&#036;[Get Code]]</a></div>
</div>

<p class='vspace'>We could modify this property slightly to instead check whether, from any state that satisfies the label "ready", we eventually reach a "done" state with probability 1. This could be done with either of the following two equivalent properties:
</p>
<div class='vspace'></div>
<div class='sourceblock ' id='sourceblock55'>
  <div class='sourceblocktext'><div class="prism"><span class="prismkeyword">filter</span>(<span class="prismident">forall</span>, "<span class="prismident">ready</span>" =&gt; <span class="prismkeyword">P</span>&gt;=<span class="prismnum">1</span> [ <span class="prismkeyword">F</span> "<span class="prismident">done</span>" ])<br/>
<span class="prismkeyword">filter</span>(<span class="prismident">forall</span>, <span class="prismkeyword">P</span>&gt;=<span class="prismnum">1</span> [ <span class="prismkeyword">F</span> "<span class="prismident">done</span>" ], "<span class="prismident">ready</span>")<br/>
</div></div>
  <div class='sourceblocklink'><a href='http://prismmodelchecker.localhost/manual/PropertySpecification/AllOnOnePage?action=sourceblock&amp;num=55' type='text/plain'>[&#036;[Get Code]]</a></div>
</div>

<p class='vspace'><strong>Note:</strong> In older versions of PRISM, the property above could be written just as <code>"ready" =&gt; P&gt;=1 [ F "done" ]</code> since the result was checked for all states by default, not just the <a class='wikilink' href='SyntaxAndSemantics.html'>initial state</a>. Now, you need to explicitly include a filter, as shown above, to achieve this.
</p>
<div class='vspace'></div><h3>Types of filter</h3>
<p>Most filters of the form <code>filter(op, prop, states)</code>
apply some operator <code>op</code> to the values of property <code>prop</code>
for all the states satisfying <code>states</code>,
resulting in a single value.
The full list of filter operators <code>op</code> in this category is:
</p>
<div class='vspace'></div><ul><li><code>min</code>: the minimum value of <code>prop</code> over states satisfying <code>states</code>
</li><li><code>max</code>: the maximum value of <code>prop</code> over states satisfying <code>states</code>
</li><li><code>count</code>: counts the number of states satisfying <code>states</code> for which <code>prop</code> is true
</li><li><code>sum</code> (or <code>+</code>): sums the value of <code>prop</code> for states satisfying <code>states</code>
</li><li><code>avg</code>: the average value of <code>prop</code> over states satisfying <code>states</code>
</li><li><code>first</code>: the value of <code>prop</code> for the first (lowest-indexed) state satisfying <code>states</code>
</li><li><code>range</code>: the range (interval) of values of <code>prop</code> over states satisfying <code>states</code>
</li><li><code>forall</code> (or <code>&amp;</code>): returns <code>true</code> if <code>prop</code> is <code>true</code> for all states satisfying <code>states</code>
</li><li><code>exists</code> (or <code>|</code>): returns <code>true</code> if <code>prop</code> is <code>true</code> for some states satisfying <code>states</code>
</li><li><code>state</code>: returns the value for the single state satisfying <code>states</code> (if there is more than one, this is an error)
</li></ul><p class='vspace'>There are also a few filters that, rather than returning a single value, return different values for each state, like a normal PRISM property:
</p>
<div class='vspace'></div><ul><li><code>argmin</code>: returns <code>true</code> for the states satisfying <code>states</code> that yield the minimum value of <code>prop</code>
</li><li><code>argmax</code>: returns <code>true</code> for the states satisfying <code>states</code> that yield the maximum value of <code>prop</code>
</li><li><code>print</code>: does not change the result of <code>prop</code> but prints the (non-zero) values to the log
</li><li><code>printall</code>: like <code>print</code>, but displays <em>all</em> values, even for states where the value is zero
</li></ul><div class='vspace'></div><h3>More examples</h3>
<p>Here are some further illustrative examples of properties that use filters.
</p>
<p class='vspace'>Filters provide a quick way to <em>print</em> the results of a model checking query for several states. In most cases, for example, a <code>P=?</code> query just returns the probability from the initial state. To see the probability for all states satisfying <code>x&gt;2</code>, use:
</p>
<div class='vspace'></div>
<div class='sourceblock ' id='sourceblock56'>
  <div class='sourceblocktext'><div class="prism"><span class="prismkeyword">filter</span>(<span class="prismident">print</span>, <span class="prismkeyword">P</span>=? [ ... ], <span class="prismident">x</span>&gt;<span class="prismnum">2</span>)<br/>
</div></div>
  <div class='sourceblocklink'><a href='http://prismmodelchecker.localhost/manual/PropertySpecification/AllOnOnePage?action=sourceblock&amp;num=56' type='text/plain'>[&#036;[Get Code]]</a></div>
</div>

<p class='vspace'>Values are printed in the log (i.e. to the "Log" tab in the GUI or to the terminal from the command-line). For small models, you could omit the final <code>states</code> argument (<code>x&gt;2</code> here) and view the probabilities from all states. You can also use PRISM's <a class='wikilink' href='../ConfiguringPRISM/OtherOptions.html'>verbose</a> mode to view values for all states, but filters provide an easier and more flexible solution.
<code>print</code> filters do not actually alter the result returned so, in the example above, PRISM will still return the probability for the initial state, in addition to printing other probabilities in the log.
</p>
<p class='vspace'>You can also use <code>print</code> filters to display lists of states. For example, this property:
</p>
<div class='vspace'></div>
<div class='sourceblock ' id='sourceblock57'>
  <div class='sourceblocktext'><div class="prism"><span class="prismkeyword">filter</span>(<span class="prismident">print</span>, <span class="prismkeyword">filter</span>(<span class="prismident">argmax</span>, <span class="prismkeyword">P</span>=? [ <span class="prismkeyword">F</span> "<span class="prismident">error</span>" ]))<br/>
</div></div>
  <div class='sourceblocklink'><a href='http://prismmodelchecker.localhost/manual/PropertySpecification/AllOnOnePage?action=sourceblock&amp;num=57' type='text/plain'>[&#036;[Get Code]]</a></div>
</div>

<p class='vspace'>prints the states which have the highest probability of reaching an error state.
However, you should exercise caution when using <code>argmax</code> (or <code>argmin</code>) on properties such as <code>P=? [ ... ]</code> (or <code>S=? [ ... ]</code> or <code>R=? [ ... ]</code>), whose results are only approximate due to the nature of the methods used to compute them (or because of round-off errors.)
</p>
<p class='vspace'>Another common use of filters is to display the value for a particular state of the model (rather than the initial state, which is used by default). To achieve this, use e.g.:
</p>
<div class='vspace'></div>
<div class='sourceblock ' id='sourceblock58'>
  <div class='sourceblocktext'><div class="prism"><span class="prismkeyword">filter</span>(<span class="prismident">state</span>, <span class="prismkeyword">P</span>=? [ <span class="prismkeyword">F</span> "<span class="prismident">error</span>" ], <span class="prismident">x</span>=<span class="prismnum">2</span>&amp;<span class="prismident">y</span>=<span class="prismnum">3</span>)<br/>
</div></div>
  <div class='sourceblocklink'><a href='http://prismmodelchecker.localhost/manual/PropertySpecification/AllOnOnePage?action=sourceblock&amp;num=58' type='text/plain'>[&#036;[Get Code]]</a></div>
</div>

<p class='vspace'>where <code>x=2&amp;y=3</code> is assumed to specify one particular state.
A <code>state</code> filter will produce an error if the filter expression is not satisfied by exactly one state of the model.
</p>
<p class='vspace'>Filters can also be built up into more complex expressions. For example, the following two properties are equivalent:
</p>
<div class='vspace'></div>
<div class='sourceblock ' id='sourceblock59'>
  <div class='sourceblocktext'><div class="prism"><span class="prismkeyword">filter</span>(<span class="prismident">avg</span>, <span class="prismkeyword">P</span>=? [ <span class="prismkeyword">F</span> "<span class="prismident">error</span>" ], "<span class="prismkeyword">init</span>")<br/>
<span class="prismkeyword">filter</span>(<span class="prismident">sum</span>, <span class="prismkeyword">P</span>=? [ <span class="prismkeyword">F</span> "<span class="prismident">error</span>" ], "<span class="prismkeyword">init</span>") / <span class="prismkeyword">filter</span>(<span class="prismident">count</span>, "<span class="prismkeyword">init</span>")<br/>
</div></div>
  <div class='sourceblocklink'><a href='http://prismmodelchecker.localhost/manual/PropertySpecification/AllOnOnePage?action=sourceblock&amp;num=59' type='text/plain'>[&#036;[Get Code]]</a></div>
</div>

<p class='vspace'>The <code>range</code> filter, unlike most PRISM expressions which are of type Boolean, integer or double, actually returns an interval: a pair of integers or doubles. For example:
</p>
<div class='vspace'></div>
<div class='sourceblock ' id='sourceblock60'>
  <div class='sourceblocktext'><div class="prism"><span class="prismkeyword">filter</span>(<span class="prismident">range</span>, <span class="prismkeyword">P</span>=? [ <span class="prismkeyword">F</span> <span class="prismident">count</span>=<span class="prismnum">10</span> ], <span class="prismident">count</span>=<span class="prismnum">0</span>)<br/>
</div></div>
  <div class='sourceblocklink'><a href='http://prismmodelchecker.localhost/manual/PropertySpecification/AllOnOnePage?action=sourceblock&amp;num=60' type='text/plain'>[&#036;[Get Code]]</a></div>
</div>

<p class='vspace'>gives the range of all possible values for the probability of reach a state satisfying <code>count=10</code>, from all states satisfying <code>count=0</code>.
As will be described below, this kind of property also results from the use of old-style (<code>{...}</code>) filters and properties on models with multiple initial states.
</p>
<div class='vspace'></div><h3>Old-style filters</h3>
<p>In older versions of PRISM, filters were also available, but in a less expressive form. Previously, they were only usable on <code><strong>P</strong></code>, <code><strong>S</strong></code> or <code><strong>R</strong></code> properties and only a small set of filter operators were permitted. They were also specified in a different way, using braces (<code>{</code>...<code>}</code>). For compatibility with old properties files (and for compactness), these forms of filters are still allowed. These old-style forms of filters:
</p>
<div class='vspace'></div>
<div class='sourceblock ' id='sourceblock61'>
  <div class='sourceblocktext'><div class="prism"><span class="prismkeyword">P</span>=? [ <span class="prismident">pathprop</span> {<span class="prismident">states</span>} ]<br/>
<span class="prismkeyword">P</span>=? [ <span class="prismident">pathprop</span> {<span class="prismident">states</span>}{<span class="prismkeyword">min</span>} ]<br/>
<span class="prismkeyword">P</span>=? [ <span class="prismident">pathprop</span> {<span class="prismident">states</span>}{<span class="prismkeyword">max</span>} ]<br/>
<span class="prismkeyword">P</span>=? [ <span class="prismident">pathprop</span> {<span class="prismident">states</span>}{<span class="prismkeyword">min</span>}{<span class="prismkeyword">max</span>} ]<br/>
</div></div>
  <div class='sourceblocklink'><a href='http://prismmodelchecker.localhost/manual/PropertySpecification/AllOnOnePage?action=sourceblock&amp;num=61' type='text/plain'>[&#036;[Get Code]]</a></div>
</div>

<p class='vspace'>are equivalent to:
</p>
<div class='vspace'></div>
<div class='sourceblock ' id='sourceblock62'>
  <div class='sourceblocktext'><div class="prism"><span class="prismkeyword">filter</span>(<span class="prismident">state</span>, <span class="prismkeyword">P</span>=? [ <span class="prismident">pathprop</span> ], <span class="prismident">states</span>)<br/>
<span class="prismkeyword">filter</span>(<span class="prismkeyword">min</span>, <span class="prismkeyword">P</span>=? [ <span class="prismident">pathprop</span> ], <span class="prismident">states</span>)<br/>
<span class="prismkeyword">filter</span>(<span class="prismkeyword">max</span>, <span class="prismkeyword">P</span>=? [ <span class="prismident">pathprop</span> ], <span class="prismident">states</span>)<br/>
<span class="prismkeyword">filter</span>(<span class="prismident">range</span>, <span class="prismkeyword">P</span>=? [ <span class="prismident">pathprop</span> ], <span class="prismident">states</span>)<br/>
</div></div>
  <div class='sourceblocklink'><a href='http://prismmodelchecker.localhost/manual/PropertySpecification/AllOnOnePage?action=sourceblock&amp;num=62' type='text/plain'>[&#036;[Get Code]]</a></div>
</div>

<p class='vspace'>Notice that the first of the four properties above (i.e. an old-style filter of the form <code>{states}</code> will result in an error if <code>states</code> is not satisfied by exactly one state of the model. Older versions of PRISM just gave you the value for the first state state satisfying the filter, without warning you about this. If you want to recreate the old behaviour, just use a <code>first</code> filter:
</p>
<div class='vspace'></div>
<div class='sourceblock ' id='sourceblock63'>
  <div class='sourceblocktext'><div class="prism"><span class="prismkeyword">filter</span>(<span class="prismident">first</span>, <span class="prismkeyword">P</span>=? [ <span class="prismident">pathprop</span> ], <span class="prismident">states</span>)<br/>
</div></div>
  <div class='sourceblocklink'><a href='http://prismmodelchecker.localhost/manual/PropertySpecification/AllOnOnePage?action=sourceblock&amp;num=63' type='text/plain'>[&#036;[Get Code]]</a></div>
</div>

<div class='vspace'></div><h3>Default filters</h3>
<p>Finally, for completeness, we show what the <em>default</em> filters are in PRISM,
i.e. how the way that PRISM returns values from properties by default
could have been achieved equivalently using filters.
</p>
<p class='vspace'>Queries of the form:
</p>
<div class='vspace'></div>
<div class='sourceblock ' id='sourceblock64'>
  <div class='sourceblocktext'><div class="prism"><span class="prismkeyword">P</span>&gt;<span class="prismnum">0.5</span> [ <span class="prismkeyword">F</span> "<span class="prismident">error</span>" ]<br/>
</div></div>
  <div class='sourceblocklink'><a href='http://prismmodelchecker.localhost/manual/PropertySpecification/AllOnOnePage?action=sourceblock&amp;num=64' type='text/plain'>[&#036;[Get Code]]</a></div>
</div>

<p class='vspace'>are the same as:
</p>
<div class='vspace'></div>
<div class='sourceblock ' id='sourceblock65'>
  <div class='sourceblocktext'><div class="prism"><span class="prismkeyword">filter</span>(<span class="prismident">forall</span>, <span class="prismkeyword">P</span>&gt;<span class="prismnum">0.5</span> [ <span class="prismkeyword">F</span> "<span class="prismident">error</span>" ], "<span class="prismkeyword">init</span>")<br/>
</div></div>
  <div class='sourceblocklink'><a href='http://prismmodelchecker.localhost/manual/PropertySpecification/AllOnOnePage?action=sourceblock&amp;num=65' type='text/plain'>[&#036;[Get Code]]</a></div>
</div>

<p class='vspace'>and queries of the form:
</p>
<div class='vspace'></div>
<div class='sourceblock ' id='sourceblock66'>
  <div class='sourceblocktext'><div class="prism"><span class="prismkeyword">P</span>=? [ <span class="prismkeyword">F</span> "<span class="prismident">error</span>" ]<br/>
</div></div>
  <div class='sourceblocklink'><a href='http://prismmodelchecker.localhost/manual/PropertySpecification/AllOnOnePage?action=sourceblock&amp;num=66' type='text/plain'>[&#036;[Get Code]]</a></div>
</div>

<p class='vspace'>are the same as either:
</p>
<div class='vspace'></div>
<div class='sourceblock ' id='sourceblock67'>
  <div class='sourceblocktext'><div class="prism"><span class="prismkeyword">filter</span>(<span class="prismident">state</span>, <span class="prismkeyword">P</span>=? [ <span class="prismkeyword">F</span> "<span class="prismident">error</span>" ], "<span class="prismkeyword">init</span>")<br/>
<span class="prismkeyword">filter</span>(<span class="prismident">range</span>, <span class="prismkeyword">P</span>=? [ <span class="prismkeyword">F</span> "<span class="prismident">error</span>" ], "<span class="prismkeyword">init</span>")<br/>
</div></div>
  <div class='sourceblocklink'><a href='http://prismmodelchecker.localhost/manual/PropertySpecification/AllOnOnePage?action=sourceblock&amp;num=67' type='text/plain'>[&#036;[Get Code]]</a></div>
</div>

<p class='vspace'>for the cases where there the model has a single initial state
or multiple initial states, respectively.
</p><hr />
<h1>PTA Properties</h1>
<p>The classes of property that can be checked for PTAs are currently more restricted than for the other kinds of models that PRISM supports. This is because the model checking procedures are quite different for this type of model. We describe these restrictions here. The situation is also dependent on which of the PTA model checking <a class='wikilink' href='../ConfiguringPRISM/ComputationEngines.html#pta'>engines</a> is being used.
</p>
<p class='vspace'>For the "<strong>stochastic games</strong>" engine, we essentially only allow unbounded or time-bounded probabilistic reachability properties, i.e. properties of the form:
</p>
<div class='vspace'></div>
<div class='sourceblock ' id='sourceblock68'>
  <div class='sourceblocktext'><div class="prism"><span class="prismkeyword">Pmin</span>=? [ <span class="prismkeyword">F</span> <span class="prismident">target</span> ]<br/>
<span class="prismkeyword">Pmax</span>=? [ <span class="prismkeyword">F</span> <span class="prismident">target</span> ]<br/>
<span class="prismkeyword">Pmin</span>=? [ <span class="prismkeyword">F</span>&lt;=<span class="prismident">T</span> <span class="prismident">target</span> ]<br/>
<span class="prismkeyword">Pmax</span>=? [ <span class="prismkeyword">F</span>&lt;=<span class="prismident">T</span> <span class="prismident">target</span> ]<br/>
</div></div>
  <div class='sourceblocklink'><a href='http://prismmodelchecker.localhost/manual/PropertySpecification/AllOnOnePage?action=sourceblock&amp;num=68' type='text/plain'>[&#036;[Get Code]]</a></div>
</div>

<p class='vspace'>where <code>target</code> is a Boolean-valued expression that does not include references to any clock variables and <code>T</code> is an integer-valued expression. The <code><strong>P</strong></code> operator cannot be nested and the <code><strong>S</strong></code> and <code><strong>R</strong></code> operators are not supported.
</p>
<p class='vspace'>The "<strong>backwards reachability</strong>" engine is similar but currently only handles maximum probabilities.
</p>
<p class='vspace'>For the "<strong>digital clocks</strong>" engine, there is slightly more flexibility,
e.g. until (<code><strong>U</strong></code>) properties are allowed, as are clock variables in expressions and arithmetic expressions such as:
</p>
<div class='vspace'></div>
<div class='sourceblock ' id='sourceblock69'>
  <div class='sourceblocktext'><div class="prism"><span class="prismnum">1</span> - <span class="prismkeyword">Pmin</span>=? [ <span class="prismkeyword">F</span> <span class="prismident">target</span> ]<br/>
</div></div>
  <div class='sourceblocklink'><a href='http://prismmodelchecker.localhost/manual/PropertySpecification/AllOnOnePage?action=sourceblock&amp;num=69' type='text/plain'>[&#036;[Get Code]]</a></div>
</div>

<p class='vspace'>This engine, however, does not yet support time-bounded reachability properties and, like the "stochastic games" engine, does not allowed nested properties. Also, references to clocks must, like in the modelling language, not use strict comparisons
(e.g. <code>x&lt;=5</code> is allowed, <code>x&lt;5</code> is not).
</p>
<p class='vspace'>The digital clocks also has support for rewards:
it is possible to check reachability reward properties of the form:
</p>
<div class='vspace'></div>
<div class='sourceblock ' id='sourceblock70'>
  <div class='sourceblocktext'><div class="prism"><span class="prismkeyword">Rmin</span>=? [ <span class="prismkeyword">F</span> <span class="prismident">target</span> ]<br/>
<span class="prismkeyword">Rmax</span>=? [ <span class="prismkeyword">F</span> <span class="prismident">target</span> ]<br/>
</div></div>
  <div class='sourceblocklink'><a href='http://prismmodelchecker.localhost/manual/PropertySpecification/AllOnOnePage?action=sourceblock&amp;num=70' type='text/plain'>[&#036;[Get Code]]</a></div>
</div>

<p class='vspace'>Reward structures specified in the model, though, must not depend on clock variables.
Formally, the class of PTAs with this kind of reward structure is sometime called <em>linearly priced PTAs</em> (see e.g. [<a class='wikilink' href='../Main/References.html#KNPS06'>KNPS06</a>].
</p>
<p class='vspace'>The digital clocks method is based on a language-level translation from a PTA model to an MDP one. If you want to see the MDP PRISM model that was generated, add the switch <code>-exportdigital digital.nm</code> when model checking property to export the model file to <code>digital.nm</code>.
</p><hr />
<h1>Properties Files</h1>
<h3>Constants</h3>
<p>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:
</p>
<div class='vspace'></div>
<div class='sourceblock ' id='sourceblock71'>
  <div class='sourceblocktext'><div class="prism"><span class="prismkeyword">const</span> <span class="prismkeyword">int</span> <span class="prismident">k</span> = <span class="prismnum">7</span>;<br/>
<span class="prismkeyword">const</span> <span class="prismkeyword">double</span> <span class="prismident">T</span> = <span class="prismnum">9.5</span>;<br/>
<span class="prismkeyword">const</span> <span class="prismkeyword">double</span> <span class="prismident">p</span> = <span class="prismnum">0.01</span>;<br/>
<br/>
<span class="prismkeyword">P</span>&lt;<span class="prismident">p</span> [ <span class="prismkeyword">F</span>&lt;=<span class="prismident">T</span> <span class="prismident">x</span>=<span class="prismident">k</span> ];<br/>
</div></div>
  <div class='sourceblocklink'><a href='http://prismmodelchecker.localhost/manual/PropertySpecification/AllOnOnePage?action=sourceblock&amp;num=71' type='text/plain'>[&#036;[Get Code]]</a></div>
</div>

<p class='vspace'>As before, these constants can actually be left undefined and then later
assigned either a single value or a range of values using <a class='wikilink' href='../RunningPRISM/Experiments.html'>experiments</a>.
</p>
<p class='vspace'>In fact, values such as the probability bounds for the <code><strong>P</strong></code> or <code><strong>S</strong></code> operators (like <code><strong>P</strong></code> above)
and upper or lower bounds for the <code><strong>U</strong></code> operator (like <code> T</code> 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.
</p>
<p class='vspace'><a name='labels' id='labels'></a>
</p><h3>Labels</h3>
<p>Another feature of properties files is <em>labels</em>. These are a way of defining sets of states that will be referred to in properties (they correspond to <em>atomic propositions</em> in a temporal logic setting). As described <a class='wikilink' href='../ThePRISMLanguage/FormulasAndLabels.html'>earlier</a>, labels can be defined in either model files or property files.
</p>
<p class='vspace'>Labels are defined using the keyword <code><strong>label</strong></code>, followed by a name (identifier) in double quotes, and then an expression which evaluates to a Boolean. Definition and usage of labels are illustrated in the following example:
</p>
<div class='vspace'></div>
<div class='sourceblock ' id='sourceblock72'>
  <div class='sourceblocktext'><div class="prism"><span class="prismkeyword">label</span> "<span class="prismident">safe</span>" = <span class="prismident">temp</span>&lt;=<span class="prismnum">100</span> | <span class="prismident">alarm</span>=<span class="prismkeyword">true</span>;<br/>
<span class="prismkeyword">label</span> "<span class="prismident">fail</span>" = <span class="prismident">temp</span>&gt;<span class="prismnum">100</span> &amp; <span class="prismident">alarm</span>=<span class="prismkeyword">false</span>;<br/>
<br/>
<span class="prismkeyword">P</span>&gt;=<span class="prismnum">0.99</span> [ "<span class="prismident">safe</span>" <span class="prismkeyword">U</span> "<span class="prismident">fail</span>" ];<br/>
</div></div>
  <div class='sourceblocklink'><a href='http://prismmodelchecker.localhost/manual/PropertySpecification/AllOnOnePage?action=sourceblock&amp;num=72' type='text/plain'>[&#036;[Get Code]]</a></div>
</div>

<p class='vspace'>Two special cases are the <code>"init"</code> and <code>"deadlock"</code> labels which are always defined.
These are true in initial states of the model and states where deadlocks were found (and, usually, fixed by adding self-loops), respectively.
</p>
<p class='vspace'><a name='names' id='names'></a>
</p><h3>Property names</h3>
<p>For convenience, properties can be annotated with <em>names</em>, as shown in the following example:
</p>
<div class='vspace'></div>
<div class='sourceblock ' id='sourceblock73'>
  <div class='sourceblocktext'><div class="prism">"<span class="prismident">safe</span>": <span class="prismkeyword">P</span>&lt;<span class="prismnum">0.01</span> [ <span class="prismkeyword">F</span> <span class="prismident">temperature</span> &gt; <span class="prismident">t_max</span> ];<br/>
</div></div>
  <div class='sourceblocklink'><a href='http://prismmodelchecker.localhost/manual/PropertySpecification/AllOnOnePage?action=sourceblock&amp;num=73' type='text/plain'>[&#036;[Get Code]]</a></div>
</div>

<p class='vspace'>which gives the name <code>"safe"</code> to the property. It is then possible to include named properties as sub-expressions of other properties, e.g.:
</p>
<div class='vspace'></div>
<div class='sourceblock ' id='sourceblock74'>
  <div class='sourceblocktext'><div class="prism"><span class="prismkeyword">filter</span>(<span class="prismident">forall</span>, <span class="prismident">num_sensors</span>&gt;<span class="prismnum">0</span> =&gt; "<span class="prismident">safe</span>");<br/>
</div></div>
  <div class='sourceblocklink'><a href='http://prismmodelchecker.localhost/manual/PropertySpecification/AllOnOnePage?action=sourceblock&amp;num=74' type='text/plain'>[&#036;[Get Code]]</a></div>
</div>

<p class='vspace'>Notice that the syntax for referring to named properties is identical to the syntax for labels. For this reason, property names must be disjoint from those of any existing labels.
</p>
<p class='vspace'>You can refer to property names when using the command-line switch <a class='wikilink' href='../RunningPRISM/ModelChecking.html#cl'><code>-prop</code></a> to specify which property is to be model checked.
</p>
<div class='vspace'></div><h3>Properties files</h3>
<p>A PRISM properties file can contain any number of properties.
It is good practice, as shown in the examples above, to terminate each property with a semicolon. Currently, this is not enforced by PRISM (to prevent incompatibility with old properties files) but this may change in the future.
</p>
<p class='vspace'>Like model files, properties can also include any amount of white space (spaces, tabs, new lines, etc.) and C-style comments, which are both ignored.
The recommended file extension for PRISM properties is now <code>.props</code>.
Previously, though, the convention was to use extension <code>.pctl</code> for properties of DTMCs, MDPs or PTAs
and extension <code>.csl</code> for properties of CTMCs, so these are still also valid.
</p>
</div>


<!--PageFooterFmt-->
  <div id='prism-man-footer'>
  </div>
<!--/PageFooterFmt-->


<!-- ============================================================================= -->

</div> <!-- id="prism-mainbox" -->

</div> <!-- id="layout-main" -->
</div> <!-- id="layout-maincontainer" -->

<div id="layout-leftcol">
<div id="prism-navbar2">

<h3><a class='wikilink' href='../Main/Main.html'>PRISM Manual</a></h3>
<p><strong><a class='wikilink' href='Main.html'>Property Specification</a></strong>
</p><ul><li><a class='wikilink' href='Main.html'>Introduction</a>
</li><li><a class='wikilink' href='IdentifyingASetOfStates.html'>Identifying A Set Of States</a>
</li><li><a class='wikilink' href='ThePOperator.html'>The P Operator</a>
</li><li><a class='wikilink' href='TheSOperator.html'>The S Operator</a>
</li><li><a class='wikilink' href='Reward-basedProperties.html'>Reward-based Properties</a>
</li><li><a class='wikilink' href='Non-probabilisticProperties.html'>Non-probabilistic Properties</a>
</li><li><a class='wikilink' href='SyntaxAndSemantics.html'>Syntax And Semantics</a>
</li><li><a class='wikilink' href='Filters.html'>Filters</a>
</li><li><a class='wikilink' href='PTAProperties.html'>PTA Properties</a>
</li><li><a class='wikilink' href='Multi-objectiveProperties.html'>Multi-objective Properties</a>
</li><li><a class='wikilink' href='PropertiesFiles.html'>Properties Files</a>
</li></ul><p>[ <a class='selflink' href='AllOnOnePage.html'>View all</a> ]
</p>


</div>  <!-- id="prism-navbar2" -->
</div> <!-- id="layout-leftcol" -->

</body>
</html>