Counter Example Analysis of Robot Action Design for Self-localization Based on Model Checking Using Probability Removed Model
Counter Example Analysis of Robot Action Design for Self-localization Based on Model Checking Using Probability Removed Model
复制标题
DOI：
10.1109/ccoms.2019.8821644
复制
发表时间：
2019-02
期刊：
影响因子：
--
通讯作者：
Ryo Watanabe;Toshifusa Sekizawa
中科院分区：
文献类型：
--
作者：
Ryo Watanabe;Toshifusa Sekizawa
网络物理系统（CPS）正在增长，并在我们的社会中发挥重要作用。 CPS集成了各种技术，例如对物理环境的计算和观察。模型检查是一种正式方法的技术，已成功应用于许多系统，以确保这些系统满足属性。我们研究了概率机器人技术中的自定位算法。在研究中，模型检查用于验证机器人位置的收敛性。剩下的一个问题是，手工分析了一些非凝结案例。在这项研究中，我们通过将概率模型转换为非稳定模型来采用反示例分析。我们显示这样的分析可以应用于机器人的设计动作。
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.