## 1 Introduction

## 2 Motivating example

## 3 Preliminaries

### 3.1 Parametric models

### 3.2 Solution functions

^{1}For instance, we may consider a solution function \(\mathsf {sol}_{\mathcal {M}}\) that maps a parameter instantiation u to the probability \(\mathsf {\mathbf {Pr}}_{{\mathcal {M}}[u]}^\text {min}(\lozenge T)\). In that case, we say that u has solution \(\mathsf {\mathbf {Pr}}_{{\mathcal {M}}[u]}^\text {min}(\lozenge T)\). Figure 3 depicts a solution function for the reachability probability \(\mathsf {\mathbf {Pr}}_{{\mathcal {M}}}(\lozenge T)\) in the pMC from Fig. 2.

### 3.3 Uncertain parametric MDPs

## 4 Problem statement

## 5 Computing the satisfaction probability

### 5.1 Obtaining solutions from parameter samples

### 5.2 Restriction to satisfying samples

^{2}, we compute a lower bound \(\eta \) on this satisfaction probability that holds with a user-specified confidence probability \(\beta \):

### 5.3 Treatment of violating samples

^{3}as a generalization that uses a fixed threshold \(\lambda \) and is also applicable in the presence of violating samples:

### 5.4 Quality of the obtained lower bounds

## 6 Derivation of the main results

### 6.1 Chance-constrained LP reformulation

### 6.2 Scenario optimization program

### 6.3 Restriction to satisfying samples

### 6.4 Treatment of violating samples

## 7 Numerical examples

Confidence probability | \(\beta = 0.9\) | \(\beta = 0.99\) | \(\beta = 0.999\) | \(\beta = 0.9999\) | ||||
---|---|---|---|---|---|---|---|---|

Weather condition | \(\eta \), sat | \(\eta \), unsat | \(\eta \), sat | \(\eta \), unsat | \(\eta \), sat | \(\eta \), unsat | \(\eta \), sat | \(\eta \), unsat |

1. Uniform distribution | 0.91138 | 0.0583 | 0.90928 | 0.0567 | 0.90735 | 0.05528 | 0.90555 | 0.05398 |

2. Stronger northbound wind | 0.77878 | 0.17483 | 0.77577 | 0.17217 | 0.77302 | 0.16978 | 0.77048 | 0.1676 |

3. Stronger westbound wind | 0.7768 | 0.17664 | 0.77378 | 0.17397 | 0.77103 | 0.17157 | 0.76847 | 0.16938 |

### 7.1 UAV motion planning

Benchmark | Instance | \(\varphi \) | #pars | Model size | Approximate (un)satisfying regions | ||
---|---|---|---|---|---|---|---|

#states | #trans | Satisfying region | Unsatisfying region | ||||

brp | (256,5) | \({\mathbf {P}}_{\le 0.5}(\lozenge T)\) | 2 | 19 720 | 26 627 | 0.055 | 0.898 |

(16,5) | \({\mathbb {E}}_{\le 3}(\lozenge T)\) | 4 | 1 304 | 1 731 | 0.275 | 0.676 | |

(32,5) | \({\mathbb {E}}_{\le 3}(\lozenge T)\) | 4 | 2 600 | 3 459 | 0.232 | 0.718 | |

crowds | (10,5) | \({\mathbf {P}}_{\le 0.9}(\lozenge T)\) | 2 | 104 512 | 246 082 | 0.537 | 0.413 |

(15,7) | \({\mathbf {P}}_{\le 0.9}(\lozenge T)\) | 2 | 8 364 409 | 25 108 729 | 0.411 | 0.539 | |

nand | (10,5) | \({\mathbf {P}}_{\ge 0.05}(\lozenge T)\) | 2 | 35 112 | 52 647 | 0.218 | 0.733 |

(25,5) | \({\mathbf {P}}_{\ge 0.05}(\lozenge T)\) | 2 | 865 592 | 1 347 047 | 0.206 | 0.744 | |

consensus | (2,2) | \({\mathbf {P}}_{\ge 0.25}(\lozenge T)\) | 2 | 272 | 492 | 0.280 | 0.669 |

(4,2) | \({\mathbf {P}}_{\ge 0.25}(\lozenge T)\) | 4 | 22 656 | 75 232 | 0.063 | 0.888 |

### 7.2 Parameter synthesis benchmarks

\(\#\) samples | Instance | 1 000 | 2 500 | 5 000 | 10 000 | 25 000 | ||||||
---|---|---|---|---|---|---|---|---|---|---|---|---|

Benchmark | \(\beta \), sat | \(\beta \), unsat | \(\beta \), sat | \(\beta \), unsat | \(\beta \), sat | \(\beta \), unsat | \(\beta \), sat | \(\beta \), unsat | \(\beta \), sat | \(\beta \), unsat | Time (s) | |

brp | (256,5) | 0.42586 | 0.14955 | 0.91278 | 0.53890 | 0.99927 | 0.91447 | 1.00000 | 0.99957 | 1.00000 | 1.00000 | 1.296 |

(16,5) | 0.05699 | 0.03247 | 0.22192 | 0.10293 | 0.62397 | 0.35332 | 0.95612 | 0.92778 | 1.00000 | 1.00000 | 0.341 | |

(32,5) | 0.05126 | 0.07365 | 0.21862 | 0.27669 | 0.50731 | 0.64205 | 0.89816 | 0.91258 | 1.00000 | 1.00000 | 0.344 | |

crowds | (10,5) | 0.04770 | 0.03339 | 0.22113 | 0.07921 | 0.58451 | 0.31034 | 0.94009 | 0.65727 | 1.00000 | 0.99943 | 0.119 |

(15,7) | 0.06568 | 0.02839 | 0.15451 | 0.05446 | 0.51860 | 0.31260 | 0.95223 | 0.71819 | 1.00000 | 1.00000 | 0.174 | |

nand | (10,5) | 0.18263 | 0.01101 | 0.62057 | 0.02775 | 0.97510 | 0.07370 | 1.00000 | 0.37567 | 1.00000 | 0.97509 | 4.097 |

(25,5) | 0.02938 | 0.20327 | 0.14312 | 0.51272 | 0.40151 | 0.82369 | 0.62267 | 0.99994 | 0.99884 | 1.00000 | 156.654 | |

consensus | (2,2) | 0.06282 | 0.02833 | 0.23683 | 0.14101 | 0.65357 | 0.44217 | 0.98990 | 0.93097 | 1.00000 | 1.00000 | 0.450 |

(4,2) | 0.13668 | 0.41820 | 0.48546 | 0.90556 | 0.86663 | 0.99999 | 0.99998 | 1.00000 | 1.00000 | 1.00000 | 26.575 |

Confidence probability | Instance | \(\beta = 0.9\) | \(\beta = 0.99\) | \(\beta = 0.999\) | \(\beta = 0.9999\) | ||||
---|---|---|---|---|---|---|---|---|---|

Benchmark | \(\eta \), sat | \(\eta \), unsat | \(\eta \), sat | \(\eta \), unsat | \(\eta \), sat | \(\eta \), unsat | \(\eta \), sat | \(\eta \), unsat | |

brp | (256,5) | 0.07244 | 0.91221 | 0.07168 | 0.91135 | 0.07099 | 0.91056 | 0.07036 | 0.90982 |

(16,5) | 0.28787 | 0.68619 | 0.28653 | 0.68481 | 0.28531 | 0.68353 | 0.28417 | 0.68234 | |

(32,5) | 0.24356 | 0.73176 | 0.24229 | 0.73044 | 0.24113 | 0.72922 | 0.24005 | 0.72808 | |

crowds | (10,5) | 0.55106 | 0.42091 | 0.54957 | 0.41945 | 0.54821 | 0.41810 | 0.54695 | 0.41685 |

(15,7) | 0.42397 | 0.54798 | 0.42250 | 0.54650 | 0.42115 | 0.54514 | 0.41990 | 0.54387 | |

nand | (10,5) | 0.23909 | 0.73637 | 0.23783 | 0.73506 | 0.23668 | 0.73384 | 0.23561 | 0.73271 |

(25,5) | 0.20979 | 0.76673 | 0.20858 | 0.76546 | 0.20748 | 0.76430 | 0.20647 | 0.76321 | |

consensus | (2,2) | 0.29383 | 0.68009 | 0.29248 | 0.67870 | 0.29125 | 0.67742 | 0.29010 | 0.67622 |

(4,2) | 0.07367 | 0.91086 | 0.07291 | 0.91000 | 0.07221 | 0.90921 | 0.07157 | 0.90846 |

## 8 Discussion and related work

^{5}[56], and finding a satisfying parameter value is exponential in the number of parameters.