Software Verification of Systematic Resampling for Optimization of Particle Filters

#systematic #resampling; #SPARK

Systematic resampling is the most popularly used resampling method in particle filters. This paper seeks to further the understanding of systematic resampling by defining a formula made up of variables from the sampling equation and the particle weights. The formula is then verified via SPARK, a software verification language. The verified systematic resampling formula states that the minimum/maximum number of possible samples taken of a particle is equal to the floor/ceiling value of particle weight divided by the sampling interval, respectively. This allows for a creation of a randomness spectrum that each resampling method can fall within. Methods on the lower end e.g. systematic resampling have less randomness, thus, are quicker to reach an estimate. Although, lower randomness allows for error by having a larger bias towards the size of the weight; having this bias creates vulnerabilities to the noise in the environment e.g. jamming. Conclusively, this is the first step in characterizing each resampling method. This will allow target-tracking engineers to pick the best resampling method for their environment instead of choosing the most popularly used one.