Abstract
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.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
References
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)
Bozzano, M., et al.: nuXmv 1.1. 1 User Manual (2016)
Coudert, O., Sasao, T.: Two-level logic minimization. In: Hassoun, S., Sasao, T. (eds.) Logic Synthesis and Verification, pp. 1–27. Springer, Boston (2002). https://doi.org/10.1007/978-1-4615-0817-5_1
Dennis, L.A., Fisher, M., Lincoln, N.K., Lisitsa, A., Veres, S.M.: Practical verification of decision-making in agent-based autonomous systems. Autom. Softw. Eng. 23(3), 305–359 (2014). https://doi.org/10.1007/s10515-014-0168-9
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_9
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)
Gainer, P., et al.: CRutoN: automatic verification of a robotic assistant’s behaviours. In: Petrucci, L., Seceleanu, C., Cavalcanti, A. (eds.) FMICS/AVoCS -2017. LNCS, vol. 10471, pp. 119–133. Springer, Cham (2017). https://doi.org/10.1007/978-3-319-67113-0_8
Ingrand, F., Ghallab, M.: Deliberation for autonomous robots: a survey. Artif. Intell. 247, 10–44 (2017)
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)
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)
Luckcuck, M., Farrell, M., Dennis, L.A., Dixon, C., Fisher, M.: Formal specification and verification of autonomous robotic systems: a survey. ACM Comput. Surv. 52, 100:1–100:41 (2019)
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
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)
Shalev-Shwartz, S., Shammah, S., Shashua, A.: Safe, multi-agent, reinforcement learning for autonomous driving. arXiv:1610.03295 [cs, stat], October 2016
Spaan, M.T.J., Veiga, T.S., Lima, P.U.: Decision-theoretic planning under uncertainty with information rewards for active cooperative perception. Auton. Agents Multi-Agent Syst. 29(6), 1157–1185 (2014). https://doi.org/10.1007/s10458-014-9279-8
Webster, M., et al.: Toward reliable autonomous robotic assistants through formal verification: a case study. IEEE Trans. Hum.-Mach. Syst. 46, 186–196 (2016)
Webster, M., et al.: Formal verification of an autonomous personal robotic assistant. In: Proceedings of the AAAI FVHMS, pp. 74–79 (2014)
Acknowledgment
This research is partially funded by the Research Fund KU Leuven. We thank the anonymous reviewers for their helpful comments.
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2020 Springer Nature Switzerland AG
About this paper
Cite this paper
Dinh, H.T., Holvoet, T. (2020). A Framework for Verifying Autonomous Robotic Agents Against Environment Assumptions. In: Demazeau, Y., Holvoet, T., Corchado, J., Costantini, S. (eds) Advances in Practical Applications of Agents, Multi-Agent Systems, and Trustworthiness. The PAAMS Collection. PAAMS 2020. Lecture Notes in Computer Science(), vol 12092. Springer, Cham. https://doi.org/10.1007/978-3-030-49778-1_23
Download citation
DOI: https://doi.org/10.1007/978-3-030-49778-1_23
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-030-49777-4
Online ISBN: 978-3-030-49778-1
eBook Packages: Computer ScienceComputer Science (R0)