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