Skip to content

Commit

Permalink
parameter doc update
Browse files Browse the repository at this point in the history
  • Loading branch information
@sjunges
sjunges committed Nov 12, 2023
1 parent 6b893d2 commit 022ca60
Show file tree
Hide file tree
Showing 11 changed files with 524 additions and 101 deletions.
52 changes: 48 additions & 4 deletions _bibliography/references.bib
View file
Original file line number Diff line number Diff line change
Expand Up @@ -5,7 +5,7 @@
PLEASE READ THIS BEFORE ADDING ENTRIES:
To easily spot duplicates, sort by
To easily spot duplicates, sort by
1. Year (descending)
2. Last name of first author
Expand Down Expand Up @@ -160,6 +160,7 @@ @inproceedings{BVKKS22


@article{CJJKT22,
category = {using},
author = {Murat Cubuktepe and
Nils Jansen and
Sebastian Junges and
Expand Down Expand Up @@ -210,6 +211,20 @@ @inproceedings{HSJMK22
arxiv-id = {2111.04407}
}

@inproceedings{JJK22,
category = {using},
author = {Nils Jansen and
Sebastian Junges and
Joost{-}Pieter Katoen},
title = {Parameter Synthesis in Markov Models: {A} Gentle Survey},
booktitle = {Principles of Systems Design},
series = {{LNCS}},
volume = {13660},
pages = {407--437},
publisher = {Springer},
year = {2022},
arxiv-id = {2207.06801}
}

@inproceedings{JS22,
category = {using},
Expand Down Expand Up @@ -345,8 +360,8 @@ @inproceedings{HJVMSV21
Sanjit A. Seshia and
Guy Van den Broeck},
title = {Model Checking Finite-Horizon {M}arkov Chains with Probabilistic Inference},
booktitle = {{CAV} {(2)}},
series = {Lecture Notes in Computer Science},
booktitle = {{CAV}},
series = {{LNCS}},
volume = {12760},
pages = {577--601},
publisher = {Springer},
Expand Down Expand Up @@ -473,6 +488,21 @@ @inproceedings{QK21
material = {https://doi.org/10.5281/zenodo.4121878},
}

@inproceedings{SJK21,
category = {feature},
author = {Jip Spel and
Sebastian Junges and
Joost{-}Pieter Katoen},
title = {Finding Provably Optimal Markov Chains},
booktitle = {{TACAS}},
series = {{LNCS}},
volume = {12651},
pages = {173--190},
publisher = {Springer},
year = {2021},

}

@inproceedings{SK21,
category = {using},
author = {Bahare Salmani and
Expand Down Expand Up @@ -605,6 +635,8 @@ @inproceedings{JKJSB20
year = {2020}
}



@inproceedings{SK20,
category = {using},
author = {Bahare Salmani and
Expand Down Expand Up @@ -731,6 +763,19 @@ @article{JAHJKQV19
website = {https://moves-rwth.github.io/prophesy/}
}

@inproceedings{SJK19,
author = {Jip Spel and
Sebastian Junges and
Joost{-}Pieter Katoen},
title = {Are Parametric Markov Chains Monotonic?},
booktitle = {{ATVA}},
series = {Lecture Notes in Computer Science},
volume = {11781},
pages = {479--496},
publisher = {Springer},
year = {2019}
}


@inproceedings{VWKN19,
category = {using},
Expand Down Expand Up @@ -1193,4 +1238,3 @@ @article{HSM97
doi = {10.1016/S0167-6423(96)00019-6},
year = {1997}
}

159 changes: 107 additions & 52 deletions documentation/usage/running-storm-on-parametric-models.md
View file
Original file line number Diff line number Diff line change
Expand Up @@ -10,108 +10,163 @@ categories: [Use Storm]

{% include includes/toc.html %}

Many model descriptions contain constants which may be specified only by an interval of possible values. We refer to these constants as parameters. Such parametric models are supported by the binary `storm-pars`. A gentle overview is given in {% cite JJK22 %}.

Many model descriptions contain constants which may be specified only by an interval of possible values. We refer to these constants as parameters. Such parametric models are supported by the binary `storm-pars`.
In what follows, we assume that all occurring parameters are graph-preserving, that is, they do not influence the topology of the underlying Markov model.
Overall, for parametric systems, various questions (henceforth: queries) relating to model checking can be asked. These different queries are supported by different engines in `storm-pars`: We refer to this as the mode -- and the mode must always be specified.

A comprehensive overview on the theoretical backgrounds is given in {% cite JAHJKQV19 %}.
The current support focusses on five modes, of which two are more experimental:
1. Feasibility -- Finding parameter values such that a property holds.
2. Verification -- Proving that for all parameter values in some region, a property holds.
3. Partitioning -- Finding regions for which the verification problem holds.
4. Solution Function computation -- Finding a closed-form representation of a solution function, mapping parameter values to, e.g., reachability probabilities.
5. Monotonicity analysis (experimental) -- Checking whether the solution function is monotonic in one of the parameters.
6. Sampling (experimental) -- Quickly sampling parametric models multiple times.

## Computing the exact solution function
We outline these modes in more detail below.
In what follows, Storm typically assumes that all occurring parameters are graph-preserving, that is, they do not influence the topology of the underlying Markov model.

To illustrate the functionality, we use a bounded retransmission protocol. This example is an adaption of the Bounded Retransmission Protocol from the [PRISM website](http://www.prismmodelchecker.org/casestudies/brp.php){:target="_blank"}. Here, we have two channels whose reliabilities are represented by parameters `pL` and `pK`.

We can run storm to obtain closed-form solutions, i.e. a rational function that represents, e.g., the probability with which the given property is satisfied for certain parameter valuations.
{% include includes/show_model.html name="parametric version of the Bounded Retransmission Protocol" class="parametric_brp" path="prism/brp.pm" %}

### Example 1 (Obtaining a closed-form solution of the parametric Knuth-Yao die)
## Feasibility
Storm currently supports two feasibility engines:
1. Parameter lifting, or just pla
2. Gradient Descent, or just gd

The following model is an adaption of the Knuth-Yao die used in previous examples.
The probability of flipping heads is now given by a parameter `p`.
While we work towards a unified interface, these support different options.

{% include includes/show_model.html name="parametric version of Knuth-Yao die" class="parametric_knuth_yao" path="prism/parametric_die.pm" %}
### Feasibility with pla

We can consider the probability of a die roll reflecting an outcome of one.
The pla engine is based on work in {% cite JAHJKQV19 %}. The feasibility computation is partially based on work in {% cite SJK21 %}.

```console
$ storm-pars --prism parametric-die.pm --prop "P=? [F s=7&d=1]"
$ storm-pars --mode feasibility --feasibility:method pla --prism brp.pm --prop 'P<=0.01 [F s=5]' --region "0.1 <= pL <= 0.9, 0.1 <= pK <= 0.9"
```
We use the `--regions` option to set the parameter region. In this case, the equivalent region could have been given using the `--regionbound 0.1`, which restricts every parameter to be bounded between `regionbound` and 1-`regionbound`.

The result is an expression over the parameter p.
The complete output to be expected is:

{% include includes/show_output.html class="closed_form_parametric_models" path="parametric/closed_form.out" %}
{% include includes/show_output.html class="pla_parametric_models" path="parametric/brp_feasibility_pla.out" %}

## Parameter lifting for region refinement
For bounded properties we can use *parameter lifting* to partition a given region into safe, unsafe and ambiguous subregions.
In particular, the output says

### Example 2 (Region refinement for a Bounded retransmission protocol)
This example is an adaption of the Bounded Retransmission Protocol from the [PRISM website](http://www.prismmodelchecker.org/casestudies/brp.php){:target="_blank"}. Here, we have two channels whose reliabilities are represented by parameters `pL` and `pK`.
```console
Result at initial state: 947822915828163/288230376151711744 ( approx. 0.003288421326) at [pK=17/20, pL=17/20].
```

{% include includes/show_model.html name="parametric version of the Bounded Retransmission Protocol" class="parametric_brp" path="prism/brp.pm" %}
which means that setting pK and pL to 17/20 yields a Markov chain such that `P<=0.01 [F s=5]` is satisfied.

We want to split our region into those subregions that result in a chance for a successful transmission that is greater than 0.5 and those that do not.
Instead of giving a bound, pla also support optimization:

```console
$ storm-pars --prism brp.pm --prop "P>0.5 [F s=5]" --region "0.1 <= pL <= 0.9, 0.1 <=pK <=0.9" --refine 0.01 10
$ storm-pars --mode feasibility --feasibility:method pla --prism brp.pm --prop 'P=? [F s=5]' --direction min --region "0.1 <= pL <= 0.9, 0.1 <= pK <= 0.9" --guarantee 0.0001 abs
```

We use the `--regions` option to set the parameter region.
The arguments we give to `--refine` are the coverage threshold and the depth limit. The coverage threshold decides how precisely we want to partition our region. The value 0.01 means that Storm will continue to refine until only 1% of the given region remains ambiguous while the rest has been determined to be either safe or unsafe. The depth limit is an optional second argument. If the level at which regions are split reaches this bound, the region is not refined any further, regardless of the coverage achieved so far.
In this case, we do not give a bound and specify with `--direction min` that we want to minimize.
Additionally, we give a `--guarantee 0.0001 abs`, specifying that we want to be find a solution which is within 0.0001 of the optimal value, where the distance is measured in absolute terms.

This produces the following output:
The complete output to be expected is:

{% include includes/show_output.html class="pla_parametric_models" path="parametric/brp_pla.out" %}
{% include includes/show_output.html class="pla_parametric_models" path="parametric/brp_feasibility_pla_guarantee.out" %}

We can see that for two parameters, Storm even visulalizes the acquired data to give an initial understanding of the region partition.
In particular, the output says

```console
Result at initial state: 5282881788238101/9223372036854775808 ( approx. 0.0005727711912) at [pK=287/320, pL=287/320].
```

This output indicates not only how to instantiate pK and pL to obtain `P=? [F s=5] = approx. 0.0005727711912`, but also that this value is within 0.0001 from the absolute lower boudn (within the given region).

### Feasibility with gd

Further options on this can be found with the following two queries:
The gd engine is based on work in {% cite HSJMK22 %}

```console
$ storm-pars --help region
$ storm-pars --help parametric
$ storm-pars --mode feasibility --feasibility:method gd --prism brp.pm --prop 'P<=0.01 [F s=5]'
```
In this case, the region for searching cannot be given.

## Monotonicity analysis
The complete output to be expected is:

Storm can also check if the parameters of a model are monotonic in regard to a certain property. For this, we use the `--monotonicity-analysis` option.
{% include includes/show_output.html class="pla_parametric_models" path="parametric/brp_feasibility_pla.out" %}

### Example 3 (Checking the monotonicity of a parameter)
Again, we use the BRP model and check if any of the parameters are monotonic:
In particular, the output says

```console
$ storm-pars --prism brp.pm --prop 'P=? [F s=5]' --region '0.1 <= pL <= 0.9, 0.1 <=pK <=0.9' --monotonicity-analysis --bisimulation
Result at initial state: 0.001706273496 ( approx. 0.001706273496) at [pK=62679533432486317/72057594037927936, pL=62679533432486317/72057594037927936].
```
We use `--bisimulation` to apply further model simplification and significantly reduce the workload of the model checker.
This results in the following output:

{% include includes/show_output.html class="mon_parametric_models" path="parametric/brp_mon.out" %}
which gives values for pK and pL such that `P<=0.01 [F s=5]` is satisfied.

If we want to take a look at the reachability order that is built during monotonicity checking, we can add the option `--mon:dotOutput` followed by an optional filename. Storm will then write a dot output of the order into the file which can then be processed using, e.g., [Graphviz](https://graphviz.org/). In this case, it results in the following graph:
## Verification
To prove the absence of a solution, we can use parameter lifting. A comprehensive overview on the theoretical backgrounds is given in {% cite JAHJKQV19 %}.

![Reachability Order]({{ '/pics/parametric-brp-mon-dot.png' | relative_url }} "Reachability Order"){: .center-image width="300"}
```console
$ storm-pars --mode verification --prism brp.pm --prop 'P<=0.9999 [F s=5]' --region "0.1 <= pL <= 0.9, 0.1 <= pK <= 0.9"
```
will provide output

For checking the monotonicity on samples, we use `--mon:samples` and provide it with the number of samples we want to be taken.

For more options on monotonictiy checking and their usages, we can use the `--help` option:
{% include includes/show_output.html class="pla_parametric_models" path="parametric/brp_verification_valid.out" %}

In contrast, running
```console
$ storm-pars --help mon
$ storm-pars --mode verification --prism brp.pm --prop 'P<=0.99 [F s=5]' --region "0.1 <= pL <= 0.9, 0.1 <= pK <= 0.9"
```
will yield output that says that the statement is *not* true:

{% include includes/show_output.html class="pla_parametric_models" path="parametric/brp_verification_invalid.out" %}


## Computing extrema
Another feature Storm offers is the computations of extrema for a property within a given region.
## Parameter Space Partitioning

### Example 4 (Extremum computation for a bounded retransmission protocol)
We reuse our BRP model from earlier to compute the maximum probability for a successful transmission that is possible in the given region.
The verification result may be too coarse: Potentially, we do want to find subregions that satisfy the property.
While we generally advocate to use our (Python) API for flexible support of such scenarios, the Storm command-line interface does yield some support:

```console
$ storm-pars --prism brp.pm --prop "P=? [F s=5]" --region "0.1 <= pL <= 0.9, 0.1 <= pK <= 0.9" --extremum max 0.01
$ storm-pars --mode partitioning --prism brp.pm --prop 'P<=0.99 [F s=5]' --region "0.1 <= pL <= 0.9, 0.1 <= pK <= 0.9"
```
We use `--extremum` and give it first a direction, in this case `max` to compute the maximum, and then a precision with which we want the maximum to be computed.

The result is the extremum as well as the specific valuation with which it was achieved.
This produces the following output:

{% include includes/show_output.html class="pla_parametric_models" path="parametric/brp_partitioning.out" %}

{% include includes/show_output.html class="extremum_parametric_models" path="parametric/brp_extremum.out" %}
We can see that for two parameters, Storm even visulalizes the acquired data to give an initial understanding of the region partition.


## Computing the exact solution function

We can run storm to obtain closed-form solutions, i.e. a rational function that represents, e.g., the probability with which the given property is satisfied for certain parameter valuations. A comprehensive overview on the theoretical backgrounds is given in {% cite JAHJKQV19 %}.

```console
$ storm-pars --mode solutionfunction --prism brp.pm --prop 'P=? [F s=5]'
```

The result is an expression over the parameter pL and pK:

```console
(-1 * (pK^10*pL^10+(-120)*pK^7*pL^7+(-10)*pK^9*pL^9+45*pK^8*pL^8+210*pK^6*pL^6+(-250)*pK^5*pL^5+(-100)*pK^3*pL^3+25*pK^2*pL^2+200*pK^4*pL^4+(-1)))/(1)
```

{% include includes/show_output.html class="closed_form_parametric_models" path="parametric/closed_form.out" %}

## Monotonicity analysis

Storm can also check if the parameters of a model are monotonic in regard to a certain property {% cite SJK19 SJK21 %}. For this, we use the `monotonicity` mode.

More relevant options can be found via

```console
$ storm-pars --help region
$ storm-pars --help parametric
$ ./storm-pars --mode monotonicity --prism brp.pm --prop 'P=? [F s=5]' --bisimulation
```

We use `--bisimulation` to apply further model simplification and significantly reduce the workload of the model checker.
This results in the following output:

{% include includes/show_output.html class="mon_parametric_models" path="parametric/brp_mon.out" %}

In particular, the output specifies that both pL and pK are monotonically decreasing.

If we want to take a look at the reachability order that is built during monotonicity checking, we can add the option `--mon:dotOutput` followed by an optional filename. Storm will then write a dot output of the order into the file which can then be processed using, e.g., [Graphviz](https://graphviz.org/). In this case, it results in the following graph:

![Reachability Order]({{ '/pics/parametric-brp-mon-dot.png' | relative_url }} "Reachability Order"){: .center-image width="300"}
Loading

0 comments on commit 022ca60

Please sign in to comment.