Deductive verification of simple foraging robotic behaviours

摘要

Purpose The purpose of this paper is to consider the logical specification, and automated verification, of high‐level robotic behaviours. Design/methodology/approach The paper uses temporal logic as a formal language for providing abstractions of foraging robot behaviour, and successively extends this to multiple robots, items of food for the robots to collect, and constraints on the real‐time behaviour of robots. For each of these scenarios, proofs of relevant properties are carried out in a fully automated way. In addition to automated deductive proofs in propositional temporal logic, the possibility of having arbitrary numbers of robots involved is considered, thus allowing representations of robot swarms. This leads towards the use of first‐order temporal logics (FOTLs). Findings The proofs of many properties are achieved using automatic deductive temporal provers for the propositional and FOTLs. Research limitations/implications Many details of the problem, such as location of the robots, avoidance, etc. are abstracted away. Practical implications Large robot swarms are beyond the current capability of propositional temporal provers. Whilst representing and proving properties of arbitrarily large swarms using FOTLs is feasible, the representation of infinite numbers of pieces of food is outside of the decidable fragment of FOTL targeted, and practically, the provers struggle with even small numbers of pieces of food. Originality/value The work described in this paper is novel in that it applies automatic temporal theorem provers to proving properties of robotic behaviour.