Assisted Counterexample-Guided Inductive Optimization for Robot Path Planning

• Mengze Li University of Manchester
• Lucas Cordeiro University of Manchester

Resumo

This paper presents and evaluates a novel offline mobile robot path planning algorithm based on the Assisted Counterexample-Guided Inductive optimization (ACEGIO) technique. ACEGIO employs a technique to assist the Counterexample-Guided Inductive optimization (CEGIO) technique by requesting counterexamples from Boolean Satisfiability (SAT) and Satisfiability Modulo Theories (SMT) solvers to improve its efficiency and effectiveness. In particular, Gradient Descent (GD) technique is implemented as an auxiliary technique to CEGIO. GD-Assisted Counterexample-Guided Inductive optimization (ACEGIO-GD) has been successfully applied to obtain two-dimensional paths for autonomous mobile robots using off-the-shelf SAT and SMT solvers. Experimental results demonstrate that the ACEGIO-based path planning algorithm has substantial improvements in efficiency and effectiveness compared to the traditional CEGIO-based path planning algorithm, which allows generating the optimal paths for autonomous mobile robots with much less execution time. If compared to other traditional path planning optimization techniques (e.g., GA and PSO), the execution time of the proposed algorithm is relatively high, whereas its performance is stable, reliable and robust.

Palavras-chave: Planing, Systems engineering and theory, Cost function, Path planning, Mobile robots, Reliability, Optimization, optimization, counterexample-guided inductive optimization, gradient descent, path planning, mobile robots