Counter Example Analysis of Robot Action Design for Self-localization Based on Model Checking Using Probability Removed Model

Cyber Physical Systems (CPSs) are growing and play important role in our society. CPSs integrate various techniques such as computation and observation of physical environment. Model checking is one technique of formal methods which has been successfully applied to many systems for ensuring these systems satisfy properties. We studied self-localization algorithm in probabilistic robotics. In the study, model checking has used to validate convergence of robot's position. One remaining problem is that some non-convergence cases are analyzed by hand. In this study, we adopt counter example analysis by converting probabilistic model to non-probabilistic model. We show such analyses can be applied to design motions of a robot.