Towards Formal Verification of Plans for Cognition-enabled Autonomous Robotic Agents

Tim Meywerk, Marcel Walter, Vladimir Herdt, Daniel Große, Rolf Drechsler

In: EUROMICRO Digital System Design Conference (DSD). Euromicro Conference on Digital System Design (DSD-2019) August 28-30 Kallithea, Chalkidiki Greece 2019.


In this paper, we propose the first approach for veri-fying plans of cognition-enabled autonomous robots that performeveryday manipulation activities in human environments. Ourmethodology is based on the new Intermediate Plan VerificationLanguage (IPVL) which is used to represent plans, environments,and robot belief states in one joint formal model. We devise asymbolic execution engine for IPVL and show the effectivenessof our overall verification methodology in a case study.

Deutsches Forschungszentrum für Künstliche Intelligenz
German Research Center for Artificial Intelligence