A Framework for Verifying Autonomous Robotic Agents Against Environment Assumptions
- 30 Downloads
Guaranteeing safety is crucial for autonomous robotic agents. Formal methods such as model checking show great potential to provide guarantees on agent and multi-agent systems. However, as robotic agents often work in open, dynamic and unstructured environments, achieving high-fidelity environment models is non-trivial. Most verification approaches for agents focus on checking the internal reasoning logic without considering operating environments or focus on a specific type of environments such as grid-based or graph-based environments. In this paper we propose a framework to model and verify the decision making of autonomous robotic agents against assumptions on environments. The framework focuses on making a clear separation between agent modeling and environment modeling, as well as providing formalism to specify agent’s decision making and assumptions on environments. As the first demonstration of this ongoing research, we provide an example of using the framework to verify an autonomous UAV agent performing pylon inspection.
KeywordsVerification Model checking Robotic
This research is partially funded by the Research Fund KU Leuven. We thank the anonymous reviewers for their helpful comments.
- 1.Aminof, B., Murano, A., Rubin, S., Zuleger, F.: Automatic verification of multi-agent systems in parameterised grid-environments. In: Proceedings of the 2016 International Conference on Autonomous Agents & Multiagent Systems. AAMAS 2016, pp. 1190–1199. International Foundation for Autonomous Agents and Multiagent Systems, Richland (2016)Google Scholar
- 2.Bozzano, M., et al.: nuXmv 1.1. 1 User Manual (2016)Google Scholar
- 5.Dixon, C., Webster, M., Saunders, J., Fisher, M., Dautenhahn, K.: “The fridge door is open”–temporal verification of a robotic assistant’s behaviours. In: Mistry, M., Leonardis, A., Witkowski, M., Melhuish, C. (eds.) TAROS 2014. LNCS (LNAI), vol. 8717, pp. 97–108. Springer, Cham (2014). https://doi.org/10.1007/978-3-319-10401-0_9CrossRefGoogle Scholar
- 6.Fu, J., Ng, V., Bastani, F., Yen, I.L.: Simple and fast strong cyclic planning for fully-observable nondeterministic planning problems. In: Twenty-Second International Joint Conference on Artificial Intelligence (2011)Google Scholar
- 9.Kouvaros, P., Lomuscio, A., Pirovano, E., Punchihewa, H.: Formal verification of open multi-agent systems. In: Proceedings of the 18th International Conference on Autonomous Agents and MultiAgent Systems. AAMAS 2019, pp. 179–187. International Foundation for Autonomous Agents and Multiagent Systems, Richland (2019)Google Scholar
- 10.Lomuscio, A., Pirovano, E.: A counter abstraction technique for the verification of probabilistic swarm systems. In: Proceedings of the 18th International Conference on Autonomous Agents and MultiAgent Systems. AAMAS 2019, pp. 161–169. International Foundation for Autonomous Agents and Multiagent Systems, Richland (2019)Google Scholar
- 12.Morse, J., Araiza-Illan, D., Lawry, J., Richards, A., Eder, K.: Formal specification and analysis of autonomous systems under partial compliance. arXiv:1603.01082 [cs], March 2016
- 13.Rubin, S.: Parameterised verification of autonomous mobile-agents in static but unknown environments. In: Proceedings of the 2015 International Conference on Autonomous Agents and Multiagent Systems. AAMAS 2015, pp. 199–208. International Foundation for Autonomous Agents and Multiagent Systems, Richland (2015)Google Scholar
- 14.Shalev-Shwartz, S., Shammah, S., Shashua, A.: Safe, multi-agent, reinforcement learning for autonomous driving. arXiv:1610.03295 [cs, stat], October 2016
- 17.Webster, M., et al.: Formal verification of an autonomous personal robotic assistant. In: Proceedings of the AAAI FVHMS, pp. 74–79 (2014)Google Scholar