Constraint Programming-Based Verification of COLREG Safety

COLREG sets maritime navigation safety rules that are defined to be human-interpretable. With the advent of autonomous surface vehicles (ASVs), the level of detail of the rules and completeness to ensure trustworthy navigation decisions by AI algorithms have become a subject of doubt. Proper interpretation of the rules presumes professional knowledge on maritime theory and practice. In particular, it concerns situations where the interpretation and application of rules is hardened due to ambiguous contextual conditions. In this article, we study the consistency and sufficiency of a subset of COLREG rules by applying constraint logic programming and formal verification techniques to identify corner cases that do not directly contradict COLREG, however, could lead to anomalous behavior of ASVs and induce safety hazards in uncommon but still possible navigation situations. As the main contribution, we expose the conditions under which ASVs could exhibit potentially deadlock and livelock-like behaviors. Namely, we exemplify the situations where uniform control decisions under the conditions of positional and movement symmetry of the vessels could lead to either infeasible trajectories or even to dangerous approaches. The identified cases portrayed with witnessing trajectory diagrams indicate potential ambiguities in the rules and could guide rules update in the future.