Advertisement

A Framework for Verifying Autonomous Robotic Agents Against Environment Assumptions

  • Hoang Tung DinhEmail author
  • Tom Holvoet
Conference paper
  • 30 Downloads
Part of the Lecture Notes in Computer Science book series (LNCS, volume 12092)

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.

Keywords

Verification Model checking Robotic 

Notes

Acknowledgment

This research is partially funded by the Research Fund KU Leuven. We thank the anonymous reviewers for their helpful comments.

References

  1. 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. 2.
    Bozzano, M., et al.: nuXmv 1.1. 1 User Manual (2016)Google Scholar
  3. 3.
    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_1CrossRefGoogle Scholar
  4. 4.
    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-9CrossRefGoogle Scholar
  5. 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. 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
  7. 7.
    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_8CrossRefGoogle Scholar
  8. 8.
    Ingrand, F., Ghallab, M.: Deliberation for autonomous robots: a survey. Artif. Intell. 247, 10–44 (2017)MathSciNetCrossRefGoogle Scholar
  9. 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. 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
  11. 11.
    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)CrossRefGoogle Scholar
  12. 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. 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. 14.
    Shalev-Shwartz, S., Shammah, S., Shashua, A.: Safe, multi-agent, reinforcement learning for autonomous driving. arXiv:1610.03295 [cs, stat], October 2016
  15. 15.
    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-8CrossRefGoogle Scholar
  16. 16.
    Webster, M., et al.: Toward reliable autonomous robotic assistants through formal verification: a case study. IEEE Trans. Hum.-Mach. Syst. 46, 186–196 (2016)CrossRefGoogle Scholar
  17. 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

Copyright information

© Springer Nature Switzerland AG 2020

Authors and Affiliations

  1. 1.Department of Computer Science, imec-DistriNetKU LeuvenLeuvenBelgium

Personalised recommendations