Department of Computer Science

Simplified form of the RANSAC algorithm

Introduction

This is the RoboChart model corresponding to the simplified form of the RANSAN algorithm in Chapter 8 of the RoboSoft paper: “RoboStar Technology: Modelling Uncertainty in RoboChart using Probability” by Jim Woodcock et al. Authors intend to use Hehner’s probabilistic predicative programming to prove this simplified form.

We use this model and its probabilistic verification using PRISM to reassure the proof is correct.

A brief description of the simplified form

Let D be a dataset and contains N data points. In order to fit a model, we need at least 2 data points. For a valid model, these data points contain at least two inliers (d=2). We also estimate the probability of one data point in D is an outlier in the model with the current parameters as q.

This model aims to determine how many iterations are needed, on average, to find the first sample without outliers for this dataset.

The paper has proved, on average, it needs 1.7 iterations for N=6 and q=1/3.

V1

Model (download)

We consider N is 6 and q is 1/3, defined as the constants in the model.

We use a uniform selection algorithm twice to randomly choose two indices from the data set as modelled in the state machine simpRansacSTM. It declares a variable i of type nat to denote the output index of the algorithm. Another two variables index0 and index1 are just the chosen indices. A value -1 indicates the index has not been chosen.

The uniform selection algorithm is implemented by a probabilistic junction between ChooseIndex and UpdateChosenIndex. The table below shows how the algorithm works and the resulted distribution.

Steps i p_{Repeat} [R] p_{UpdateChosenIndex} [U] Accumulation
1 0 5/6 [R] 1/6 [U] 1/6 [U]
2 1 4/5 [R] 1/5 [U] 5/6*1/5 = 1/6 [RU]
3 2 3/4 [R] 1/4 [U] 5/6*4/5*1/4 = 1/6 [RRU]
4 3 2/3 [R] 1/3 [U] 5/6*4/5*3/4*1/3 = 1/6 [RRRU]
5 4 1/2 [R] 1/2 [U] 5/6*4/5*3/4*2/3*1/2 = 1/6 [RRRRU]
6 5 0 [R] 1/1 [U] 5/6*4/5*3/4*2/3*1/2*1 = 1/6 [RRRRRU]

As you can see, we get a uniform distribution on i: [(0, 1/6), (1, 1/6), (2, 1/6), (3, 1/6), (4, 1/6), (5, 1/6)].

Using this algorithm with a binary choice operator P, we can implement a uniform distribution for any number of N.

Analysis

Generated PRISM model (download)

Used configuration file.

Assertions

The assertion file (download) that is used for verification is shown below.

Reports

The verification results are displayed in the report below.


Results of analysis of assertions in ransac.assertions using PRISM

Assertion: P_deadlock_free

Assertion States Transitions Time Result
P_deadlock_free 591 686 0.002 seconds true

Assertion: P_nr_of_tries

Assertion States Transitions Time Result
P_nr_of_tries 591 686 0.039 seconds 1.6998580815632656

Assertion: P_nr_of_choices

Assertion States Transitions Time Result
P_nr_of_choices 591 686 0.027 seconds 2.6998493976687925

The result of P_nr_of_choose gives us the average number of occurrences of the choose event: 2.6998.

The result of P_nr_of_tries gives us the average number of entries to the badFit state: 1.6998, which is consistent with the result 1.7 by theorem proving.

V2

Model (download)

In this version, we use an operation ChooseUniform to implement the uniform selection algorithm.

Then in the state machine, this operation is called twice to select indices for index0 and index1.

Analysis

Generated PRISM model (download)

Used configuration file.

Assertions

The assertion file (download) that is used for verification is shown below.

Reports

The verification results are displayed in the report below.


Results of analysis of assertions in ransac.assertions using PRISM

Assertion: P_deadlock_free

Assertion states: transitions: result: checkTime:
P_deadlock_free 3615 4070 true 0.003 seconds

Assertion: P_nr_of_tries

Assertion states: transitions: result: checkTime:
P_nr_of_tries 3615 4070 1.6998561958204306 0.117 seconds

Assertion: P_nr_of_choices

Assertion states: transitions: result: checkTime:
P_nr_of_choices 3615 4070 2.6998527952527036 0.115 seconds

Assertion: P_goodfit

Assertion states: transitions: result: checkTime:
P_goodfit 3615 4070 1.0 0.043 seconds

The results of P_nr_of_choose and P_nr_of_tries of V2 are consistent with those of V1.

Conclusion

This example shows the probabilistic analysis of a RoboChart model by modeling checking can be used in a complementary way to theorem proving.

In the future, we will bring the proving capability into RoboTool, and so we can use both model checking and theorem proving for analysis together.

Department of Computer Science
Deramore Lane, University of York, Heslington, York, YO10 5GH, UK
Tel: 01904 325500