Towards Verification of Robot Design for Self-localization

摘要

CPS plays important roles along with popularization. In this study, we handle an autonomous robot which estimates its position by observations in discrete two-dimensional field. Probabilistic behaviors are modeled in MDPs, and model checking results validate robot's design.