Autonomous vessel collision avoidance verification using geometric optimization

Abstract

The rapid advancement of Maritime Autonomous Surface Ships (MASS) has highlighted the necessity of revisiting the International Regulations for Preventing Collisions at Sea (COLREG), as the current framework does not fully account for the operational and decision-making challenges introduced by autonomous navigation. This paper extends our previous work on maritime safety by explicitly incorporating relative speed variations between vessels, whereas the earlier study was limited to encounter scenarios involving ships with identical speeds. When the analysis assumptions were relaxed, it was necessary to adapt the calculation of other navigation-related parameters, such as the collision angle, to evaluate how speed differences influence the collision-risk geometry. As in our earlier approach, the derived analytical constraints are used to reduce the constraint space explored by Constraint Logic Programming (CLP) to uncover potential gaps and ambiguities in COLREG compliance for MASS. We also refine our geometric optimization method further to restrict the search space in standard navigation situations. By focusing on two-dimensional spatial parameters within a bounded surface domain, the extended approach preserves near-polynomial search complexity while enabling a more realistic and comprehensive analysis of vessel encounter situations safety. According to the performance analysis, the identification of adversary vessel positions that lead to close encounter prediction requires less than a half second, which is sufficient to be deployed onboard navigation warning system.

Keywords

maritime autonomous surface ships COLREG compliance safety verification constraint logic programming geometric constraints state-space search optimization

1 Introduction

Although the collision avoidance objective is widely acknowledged in mobile robotics, given that the safety of both the mobile systems themselves and the entities they carry depend on it, the solutions for its implementation are highly diverse and largely context-dependent. Indeed, algorithms that are effective for robots navigating in a planar environment with dynamic obstacles Estevez et al.¹ do not meet the requirements of a fleet of vehicles whose task allocation evolves over time Grosset et al.² or of a system operating in a three-dimensional environment with static obstacles Tavaris et al.³ Furthermore, such algorithms must account for the dynamics that is specific to the moving system itself. For instance, a bipedal robot Liu et al.⁴ is subject to different constraints than a wheeled robot or a vessel with high inertia.

Timely and reliable navigation decisions in challenging maritime environments affected by weather conditions, sensor failures, or AIS data spoofing are essential for ensuring safety for both human-operated and autonomous vessels. Avoiding close-quarter situations (CQS) becomes even more complex in mixed traffic involving Maritime Autonomous Surface Ships (MASS) Vain et al.⁵ The COLREG, established in the 1970s, provides general guidelines for collision avoidance; however, technological advances, increasing traffic density, and the rise of autonomous navigation have created a need to reassess these regulations for compatibility with both human navigators and autonomous control algorithms.

Simulation-based methods such as ISTA testing and sea trials provide valuable insights but fail to generalize across the full spectrum of possible maritime scenarios. Formal verification techniques offer exhaustive results but become computationally challenging, especially for NP-complete problems such as planning safe maneuvers in multi-vessel encounters Reif.⁶ Our previous work Lahbib et al.⁷ introduced a compositional approach that uses geometric constraints within Constraint Logic Programming (CLP) to analyze COLREG-compliant behaviors. By focusing on critical vessel pairs, the approach reduces the analysis complexity to a near-polynomial function of the number of encounter situations.

This article extends our previous work Lahbib et al.⁷ in several ways. First, we revise the formalization of the navigation model by introducing heterogeneous vessel speeds in encounter situations, replacing the earlier assumption of equal speeds. This change requires reformulating the geometry of the collision trajectories and recalculating key parameters, including an angle between collision courses of vessels.

Our earlier CLP-based verification approach relied on deterministic search, which offers predictability and interpretability but suffers from limited flexibility, potential incompleteness, and poor scalability with large or disjunctive constraint sets Hanus and Sacerdoti Coen.⁸ In contrast, nondeterministic and stochastic search strategies—such as random search, genetic algorithms, and simulated annealing—provide better scalability and flexibility for exploring complex constraint spaces Refalo⁹; Cicirello and Smith.¹⁰ Local search methods further improve solution quality by iterating candidate refinement Pretschner.¹¹ However, a key challenge across all approaches remains. It is effective management of decision procedures algorithmic complexity and the reduction of constraints solving search space without compromising decision quality. In this work, we investigate ways to reduce the complexity of parameters’ domain exploration by CLP associated with COLREG-governed navigation. After identifying relevant headings, speed, and positional parameters, we introduce geometric feasibility constraints that significantly reduce the solution search space by eliminating irrelevant configurations that cannot lead to encounter situations of interest. Second, based on these relaxed model conditions, we redesign the critical navigation constraint generation software to handle the new parameter relations in the model accurately. Finally, we perform a new evaluation on the revised model, demonstrating how these additions influence the search space and the identification of encounter situations specified in COLREG. Our updated implementation and new evaluation show that the approach achieves on average a 90% reduction in the search space while also improving the explanatory clarity of factors leading to encounter situations through the revised formalization and the elaborated parametric constraint system. The time required to identify the reduced search space is less than 0.35 s in the worst case, which demonstrates the relevance of the performance for MASS’ collision early warning system.

The remainder of this paper is organized as follows.

Section 2 reviews related work. Section 3 introduces COLREG-regulated navigation situations, maneuvering parameters, and theoretical preliminaries on CLP and search techniques. Section 4 presents our constraint-space reduction method, with a focus on the generalized collision-area equations. Section 5 outlines the search space reduction algorithms. Section 6 describes the method evaluation and complexity analysis. Section 7 discusses the scope and possible restrictions to the applicability of the method. Finally, Section 8 concludes and describes future work.

2 Related work

Constraint logic programming over a finite domain relies on implicit enumeration with three main search strategies, namely: generate and test, early pruning, and labeling. In Boizumault et al.,¹² the authors have used constraint logic programming in finite domains to efficiently solve the examination timetabling problem. They have defined five categories of constraints: Variable domains, incompatibility, precedence, time, and capacity. In this proposal, the authors tested two labeling strategies, FirstFail and Best-Fit-Decreasing, for two different approaches. In the former approach, room capacities were verified a posteriori, following the labeling process. In the latter, the authors used the cumulative constraint, as they stated the capacity constraint before the labeling stage. The second strategy has led to better pruning of the search tree. Unlike our approach, the constraints described by this research do not address geometric aspects where trigonometric functions involve non-finite variable domains.

The Euclidean Traveling Salesperson Problem (ETSP) is a special case of TSP in which each node is identified by its coordinates on the plane and the Euclidean distance is used as the cost function. Papadimitriou.¹³ Similarly, Bertagnon and Gavanelli¹⁴ exploited geometric information to improve constraint propagation for solving the ETSP problem. They defined new constraints to avoid crossings, eliminate aligned points, and perform symmetry breaking. They also made use of the convex hull method Graham,¹⁵ which computes the smallest convex set that encloses all the points, forming a convex polygon. In Bellodi et al.,¹⁶ the authors have used a binary classifier to reduce the complexity of the constraints by retaining those that are effective. The collision conditions can be defined by two constraints constructed from the complement of those describing crossing and alignment avoidance. Unlike their work, we couple these constraints into a single constraint that characterizes the collision and allows a drastic reduction of the search space. Hu et al.¹⁷ presented a multi-objective optimization approach for trajectory planning of Autonomous Surface Vehicles (ASVs), considering Collision Avoidance and COLREG rules. The COLREG rules and physical constraints were formulated as mathematical inequalities. A multiobjective optimization problem was then solved using particle swarm optimization. The system consisted of a global path planner and a local path planner. The global planner generated the path offline as a sequence of waypoints, and the local, online planner was invoked if obstacles were detected between any two waypoints, generating a path from the current position to the next waypoint. Situational awareness and risk management were implemented by applying a Closest Point of Approach (CPA)-based method. The approach was validated through simulations accounting for multi-vessel scenarios as well as for non-COLREG-compliant vessels. Simulations in which practical issues such as measurement noise, disturbance, and vehicle dynamics are explicitly taken into account are mentioned to be presented in the future. We argue that such an approach can provide nonoptimal solutions when retaining the global waypoints in the obstacle avoidance maneuver. Namely, this strategy may force returning backwards or taking unnecessary round-trips when returning to the next waypoint of the global course. In maritime practice, shortcutting from the earliest point of obstacle detour back to chosen waypoint of the global trajectory, not just to any specific unattended waypoint, is applied. Pedersen et al.¹⁸ has provided a method and software toolbox for generating ship encounters to systematically assess the vessel's ability to act according to COLREG. They provide a set of 20 single cases to handle collision situations. The approach described in their paper simulates each valuation of the parameter vector as a separate case, with the scope of these cases not explicitly bounded.

In verification, we need state space exhaustive exploration and not only simulation-based verification as proposed by Pedersen et al.,¹⁸ which is studying predefined cases based on specific parameters setting (not ranges of values), e.g., baseline cases: head-on (HO), crossing-give-way (CRGW), crossing-stand-on (CR-SO), overtaking-give-way (OTGW), and overtaking-stand-on (OT-SO). Thus, this approach is not an exhaustive exploration method in general such as our method, which covers all the baseline cases mentioned above. Moreover, Pedersen et al. proposition needs the definition of exponentially increasing number of baseline cases in the number of ships.

In contrast to optimization-based or learning-driven approaches, several foundational works rely on analytical geometry to characterize encounter situations. Like in our work, the velocity-obstacle formulation introduced by Fiorini and Shiller¹⁹ models collision risk through the direction of the relative velocity vector, providing a purely kinematic characterization of potential conflicts. In the maritime domain, Tam et al.²⁰ surveyed collision-avoidance and path-planning methods for ships in close-range encounters, highlighting the importance of angular and kinematic reasoning when assessing COLREG compliant maneuvers. In contrast, our study derives a closed-form analytical expression for the collision angle δ from the general relative velocity vector V _r = V _A − V _B , thereby allowing heterogeneous vessel speeds to be explicitly embedded within a constraint-based framework. By enforcing these analytical constraints, the admissible solution space is confined to configurations that satisfy welldefined geometric and kinematic conditions. This targeted restriction substantially reduces the CLP search space by ensuring that simulation and verification are applied exclusively to analytically valid scenarios, thereby enhancing both computational efficiency and overall accuracy of the verification results.

Recent advances in formal verification and reachability analysis Krasowski and Althoff,²¹ have been applied to autonomous navigation and safety-critical systems and demonstrated a potential of exhaustive parameter space coverage, but at the downside is the need for substantial simplification of modeling assumptions. On the other hand, approaches Shokri-Manninen et al.;²² Ge et al.;²³ Miao et al.²⁴ based on hybrid-system verification and reachable set computation provide strong guarantees on system behavior under dynamic constraints. Tools such as Uppaal Stratego, SpaceEx, and Flow* enable analysis of hybrid systems with nonlinear dynamics. In the context of autonomous navigation, these methods have been used to verify safety properties and collision avoidance strategies in robotic and maritime systems. The tradeoff between over approximated assumptions and fine-grained hybrid dynamic models, which demand high complexity verification algorithms, a CLP-based method Vain et al.⁵ was proposed for verification of maritime incidents due to its expressive power and efficient reasoning mechanism. The present work relies on this paper to reduce the combinatorial complexity of constraint-based verification through geometric pruning, complementing the abovementioned approaches by enabling efficient exploration of collision-prone approach configurations.

3 Preliminaries

3.1 Maritime navigation regulations COLREG

International maritime regulations for avoiding collisions at sea, COLREG IMO²⁵; Eriksen et al.²⁶ are defined to be human interpretable. However, the adequacy of COLREG for MASS has been questioned due to concerns about its level of detail and completeness for safe navigation.

Accurate interpretation of navigational rules requires expert maritime knowledge, while the implementation of autonomous navigation decisions demands a level of specification that exceeds what is currently provided by COLREG. This limitation is particularly pronounced for Rules 6 and 13–17, where context-dependent and ambiguous conditions significantly complicate their formal interpretation. Rule 6 requires vessels to maintain a safe speed to avoid collisions and to stop within an appropriate distance, considering weather, draft, fairway, and maneuverability.

Rules 13–15 (see Figure 1) govern vessel encounter situations. Specifically, Rule 13 requires an overtaking vessel to give way, Rule 14 prescribes a starboard alteration of course in head-on encounters, and Rule 15 obliges a vessel to give way when crossing from the port side of another vessel. Rules 16 and 17 further define the respective responsibilities of give-way and stand-on vessels, mandating early and substantial action by the give-way vessel to avoid collision, while requiring the stand-on vessel to take appropriate action if the give-way vessel does not comply.

While the COLREG rules give human-readable guidelines for helmsmen on what to do in a navigation situation, they leave relative freedom to decide how to apply the rule. For example, the rules state that the speed should be adjusted to be able to stop within an ‘appropriate’ distance; actions should be taken ‘as early as possible’. For autonomous vessels, instructions without quantification could easily lead to unpredictable, potentially hazardous situations. Thus, to ensure MASS's correct behavior in terms of COLREG rules and good seamanship, its decisions need to be formulated in quantitative terms and implemented in the navigation controller as an unambiguous and consistent rule system.

Even implementing the MASS decision engine with heuristic expert rules may not always remove uncertainties in handling all edge cases. Though often useful, the purely heuristic rules may still leave gaps in reasoning and allow loose interpretations of terms such as “appropriate distance” and “as early as possible”. Probabilistic, fuzzy, or interval logic-based decision mechanisms provide “measurable” uncertainty of inferred decisions. However, more deterministic decision-making requires even stronger analytical models embedded in a logically consistent and complete constraint system that are adaptable to variable contexts.

3.2 Constraint logic programming

This work formalizes COLREG rules and enhances them through quantitative refinement to support the safety assessment of MASS navigation. The proposed framework combines (i) CLP to formally define and restrict the navigational search space, and (ii) constraint-solving techniques to verify the safety of maneuvering decisions under predefined constraints and temporal limits.

CLP is a programming paradigm that merges two declarative paradigms: constraint solving and logic programming Marriott et al.²⁷ CLP programs, in general, are evaluated by model generation, so that the program clauses are used both for generating the search space and for constraining it. CLP is an instance of the general Constraint Satisfaction Problem (CSP), namely, programming and solving constraints over variables whose domains are Herbrand terms. Given a problem description, a constraint solver tries to find valid solutions via constraint propagation and search Popescu et al.²⁸ Our approach models navigation using a constraint system, defining parameters with boundary values (e.g., speed limits, turning radius) and relational constraints. Constraint satisfaction is checked through variable labeling functions that handle constraint propagation and instantiation strategies In its general setting, CSP comprises a set of variables X = x₁,…,x_n, possible value sets D(x_i) for each variable known as the variable domain, and relations between these variables in the form of constraint sets Van Roy.²⁹ Constraint propagation filters out inconsistent domain elements to ensure consistency but often requires additional search to narrow down the solutions. Due to complexity issues, solving a CSP requires balancing constraint propagation with computational efficiency Triska.³⁰ Labeling is a CLP method that assigns values to variables, further refining the search space and guiding the search over the solution space. When a CSP problem is implemented in a CLP platform, constraints are represented as logic programs. In this study, COLREG safety constraints are formalized as first-order Horn clauses that define relationships among navigational parameters. Variables represent decision parameters to be determined, while predicates encode vessel characteristics, obstacles, and navigational constraints. Constraint solving consists of identifying variable assignments that satisfy these constraints, which are partially instantiated by contextual parameters that evolve dynamically over time. This paper specifically focuses on search space reduction, demonstrating that even modest strengthening of conjunctive constraints on vessel speed and course (further called feasibility constraints) can substantially improve the efficiency of constraint solving.

3.3 Collision verification framework (CVT)

To support the formal analysis of collision-prone maritime scenarios, we introduce a domain-specific verification framework, referred to as the Collision Verification Tool (CVT). The architecture of the framework is illustrated in Figure 2 and follows a layered design separating application, verification, and execution concerns.

Figure 1.

COLREG rules 13–15 and 17: stand-on vessels (gray).

Figure 2.

Layered architecture of the collision verification tool (CVT).

At the application layer, a modeling tool provides vessel parameters (position, heading, speed), environmental conditions (e.g., sea state, leeway), and navigational context, defining the initial configuration space. This layer also enables interaction with external simulation environments through a middleware interface.

The core of the framework is the verification layer, which implements the CVT components. The Explorer module generates candidate scenarios by enumerating combinations of vessel states within bounded domains using CLP(FD)³¹ strategies. A key contribution of this work is the integration of a Geometric Optimization module within the Explorer, which introduces analytically derived constraints to prune infeasible configurations (and excluding spurious solutions) prior to verification. The Solver evaluates the remaining configurations by applying constraint propagation and logical inference to verify compliance with collision avoidance rules derived from COLREG. The Middleware Interface enables bidirectional communication with external simulators, allowing selected scenarios to be refined and validated in higher-fidelity environments on demand.

At the execution layer, constraint solving is supported by a CLP(FD) engine deployed on a computational platform that may operate onboard or in cloud environments, ensuring scalability and efficient processing.

In a baseline setting without geometric optimization, the Explorer exhaustively generates configurations that satisfy domain constraints, and the Solver verifies each configuration independently. While this guarantees completeness, it leads to a large number of configurations being evaluated and therefore high computational cost.

With the integration of geometric optimization, the interaction between components is significantly modified. The pruning of infeasible configurations is performed early in the exploration process, ensuring that only configurations likely to lead to close-quarters situations are forwarded to the Solver for constraints satisfiability check and witness traces generation. This reduces the search space while preserving correctness, thereby improving the efficiency of the overall verification process.

Furthermore, the introduction of the middleware layer enables a two-level analysis approach Lahbib et al.³² The CVT framework performs a fast, analytical exploration of the configuration space, while selected critical scenarios can be further analyzed using external simulators, e.g., Open Simulation Platform (https://opensimulationplatform.com/), where vessel specific dynamics, energy use, and other physical parameters are involved. This combination allows the framework to balance computational efficiency with higher-fidelity evaluation, improving its applicability in realistic maritime navigation contexts.

Thus, the resulting framework combines CLP(FD)-based exploration with domain-specific geometric pruning and middleware-based refinement, forming a hybrid verification mechanism that integrates discrete constraint reasoning, continuous geometric analysis, and system-level simulation.

The proposed framework has open architecture and is well-suited for validating the underlying mathematical and geometric formulations of collision-prone scenarios. While the current evaluation focuses on analytically controlled settings, further integration with realistic maritime environments can enhance its practical representativeness in operational contexts.

This middleware-based architecture facilitates the incorporation of real-time data streams and external decision support modules, thereby enhancing the applicability of the framework in realistic maritime navigation contexts.

4 Problem formalization

4.1 Hypothesis identification

As constraint solving presumes exploring multi-dimensional model state space, this section details the strategy we adopted to optimize space exploration related to the vessels’ entry positions on the modeling canvas and eliminating those initial positions that clearly exclude collisions and close quoter approaches within the model time span. We address the complexity reduction problem of the exploration algorithm as a multivariate optimization problem. The following Listing 1 defines the parameters of a variable domain to explore, along with its exploration strategy encoded in the CLP clause domain/4, where domain denotes the functor and /4 arity of the clause.

Listing 1: Prolog fact template describing the domain of a variable and its exploration rule

%−−−−−−−−−− domain/4 −−−−−−−−−−%

% TEMPLATE: domain(Var,Dom,DomSharingConstr, UpdateConstr)

% Var ::=((ClauseFunct,Entity\_ID, NofEntityInstances), ArgNo)

% Dom ::=((LB,UB),Granularity)

% DomSharingConstr ::=(DistrConstr, Delta)

% UpdateConstr ::=(Initial, StepLength, StepDirect,StopCond)

Since each parameter of domain/4 consists of subparameters, grounding the whole clause requires handling 13 dimensions. Checking all parameter combinations is NP-hard. To reduce the search space, we first optimize each parameter separately, then apply constraints to define dependencies which allow further reduction. The first parameter of the domain clause, denoted by Var, is a pointer to a clause, in which the parameter we explore occurs. For instance, the parameter referred in the clause ClauseFunct of V ar/2 occurs in the fact ship0/7, the template of which is depicted in the Listing 2.

Listing 2: Prolog comments of the first domain parameter template

%−−−−−−−−−− ship 0/7 −−−−−−−−−−%

% ship0(ID,Dimensions,Timestamp,(X,Y), COG,SOG,Under\_ctrl)

The first parameter ID of ship0 denotes unique identifier of the model entity ship, while the second specifies the ship's dimensions (length, beam, draft). The remaining five parameters relate to the ship's behavior. The timestamp represents the time the ship appears at position (X,Y) and COG and SOG specify the course and speed over ground, at that time step. The last parameter, Underctrl, indicates the ship's controllability, distinguishing between full control and issues like thruster failures or AIS data spoofing that could compromise the ship's adequate control actions.

The position, (X,Y), depends on the canvas (modeled area) size, with width W and length L, and granularity (gran). COG ranges from 0 to 360 degrees, and speed ranges from 0 to 25 knots, both with the finest granularity step of one unit.

For this parameter setting, equation (1) shows the number of combinations of possible parameter initializations for just one vessel in such a modeling setup. Even though this value is constant, it is large enough to impact the complexity of exhaustive search when studying the simultaneous behavior of multiple ships on canvas.

\begin{aligned} N_{C o m b .} & = (\begin{matrix} 25 \\ 1 \end{matrix}) (\begin{matrix} \frac{W x L}{g r a n^{2}} \\ 1 \end{matrix}) (\begin{matrix} 360 \\ 1 \end{matrix}) (\begin{matrix} 26 \\ 1 \end{matrix}) \\ = \frac{W x L}{g r a n^{2}} 2, 34 \cdot 10^{5} \end{aligned}

(1)

Thus, the number of possible parameter groundings in clausal constraints (counted as grounded clause instances) increases exponentially with the number of vessels (i.e., n_vessels in equation (2)) and with the parameters of other entities involved in the constraints, such as additional ships, as depicted in equation (2).

N_{C l a u s e F u n c t o r} = (N_{C o m b .})^{n_{v e s s e l s}}

(2)

To overcome the exponential growth of parameter groundings in facts domain/4 and ship0/7, we narrow the vessel parameter domains using auxiliary feasibility constraints. The goal is to find values that define maneuvers potentially leading to collisions, eliminating those not involving close-quarter situations.

Hence, we need to define the initial conditions under which the likelihood of a collision exists on the canvas. While in general, collision conditions depend on numerous factors, such as vessels’ speed, heading, initial position, and many others, we demonstrate that the problem complexity can be reduced drastically by applying the ‘divide and conquer’ principle, i.e., by decomposing those conditions into cases where the constraints are strengthened with a few straightforward and simple hypotheses such as:

Crossing conditions for two vessels (i. e. n_vessels = 2),

Vessels dimensions are constant,

Vessels’ cruising speeds are constant but different,

Vessels headings are constant, and

Vessels’ initial positions differ by a distance greater than the critical threshold of Close Quarter Situation (CQS).

Under these assumptions, the reduction strategy can be directed toward the term ${(\frac{W \times L}{g r a n})}^{2}$ , which provides an approximation of the upper bound on the number of possible initial position pairs for two vessels within the canvas. It is an upper bound because we assume that the ships are initially located not closer to each other than the distance defined by COLREG as CQS, i.e., a critical separation between a pair of vessels from the so-called own ship (e.g., in Figure 3, ship A).

4.2 Geometric formulation

To obtain the Cartesian equation of the ray, representing in our setting a segment of initial positions of ship B, we need to determine the slope angle δ.

In the classical geometric construction based on a general triangle ACB, δ was obtained from an assumed symmetry of this triangle. In this work, we refine and generalize this derivation using the kinematics of relative motion between the two vessels.

Figure 3 represents the velocity vectors V _A , V _B , ships relative velocity vector V _r , and the angles α, β and δ, showing the construction that leads to the unified expression of δ. This graphical representation provides a clear geometric interpretation of the first boundary delimiting the initial positions of Ship B relative to Ship A.

Figure 3.

Geometric illustration of the velocity vectors and resulting boundary for the initial position of ship B.

The velocity vectors of ships A and B in Cartesian coordinates are

\begin{aligned} V_{A} & = (V_{A} c o s α, V_{A} s i n α), \end{aligned}

\begin{aligned} V_{B} & = (V_{B} c o s β, V_{B} s i n β), \end{aligned}

where α and β denote the respective headings with respect to the x-axis, and V_A, V_B are their speed magnitudes. The relative velocity of ship B with respect to ship A is

V_{r} = V_{A} - V_{B},

with components

\begin{aligned} V_{r, x} & = V_{A} c o s α - V_{B} c o s β, \end{aligned}

\begin{aligned} V_{r, y} & = V_{A} s i n α - V_{B} s i n β . \end{aligned}

The direction δ of the potential initial positions of ship B coincides with the half-line orientation of the relative velocity vector V _r .

From the definition of the tangent of a planar vector,

\tan δ = \frac{V_{r, y}}{V_{r, x}},

and substitution yields

\tan δ = \frac{V_{A} \sin α - V_{B} \sin β}{V_{A} \cos α - V_{B} \cos β}

Numerically robust computation using atan2. Although δ could in principle be obtained using the single-argument arctangent,

δ = \arctan (\frac{V_{A} \sin α - V_{B} \sin β}{V_{A} \cos α - V_{B} \cos β}),

this ratio is ill-conditioned when the denominator becomes small and does not resolve quadrant ambiguities. To ensure numerical stability and correct quadrant identification, we compute δ directly using the two-argument arctangent which evaluates the horizontal and vertical components simultaneously, avoids division by zero when V_r,x = 0, and assigns δ to the proper quadrant. This yields the unified expression

δ = a t a n 2 (V_{A} \sin α - V_{B} \sin β, V_{A} \cos α - V_{B} \cos β),

(3)

valid for arbitrary speeds V_A and V_B.

Special case: equal speeds. If both ships move at the same speed,

V_{A} = V_{B} = V,

the components of V _r reduce to

\begin{aligned} V_{r, x} & = V (c o s α - c o s β), \end{aligned}

\begin{aligned} V_{r, y} = V (s i n α - s i n β) . \end{aligned}

Using standard trigonometric identities,

\begin{aligned} \cos α - \cos β & = - 2 \sin (\frac{α + β}{2}) \sin (\frac{α - β}{2}) \end{aligned}

\begin{aligned} \sin α - \sin β & = 2 \cos (\frac{α + β}{2}) \sin (\frac{α - β}{2}) \end{aligned}

we obtain

\tan δ = - \cot (\frac{α + β}{2}) .

Since cotθ = tan(90° − θ),

\tan δ = \tan (- 90 \circ + \frac{α + β}{2}),

and therefore, modulo 180°,

δ = - 90 \circ + \frac{α + β}{2} (m o d 180 \circ) .

(4)

This matches exactly the geometric construction previously used in the model, demonstrating that it is a special case of the general kinematic formulation (3).

Cartesian equation of the collision half-line. The halfline originating at ship A at position (x_A,y_A) and oriented with angle δ has the Cartesian representation

y = t a n (δ) x + y_{A} - t a n (δ) x_{A} .

(5)

The physically relevant branch is determined by the sign of the horizontal component:

\begin{aligned} x & > x_{A} i f - 90 \circ < δ < 90 \circ, \end{aligned}

\begin{aligned} x & < x_{A} i f 90 \circ < δ < 270 \circ . \end{aligned}

Only this forward direction, aligned with the relative motion, is used in the collision analysis.

After identifying the first limit of the initial positions of Ship B related to Ship A, provided by equation (5), we will characterize the second limit to define the segment endpoint or beginning point. The exploration space is defined by square, delimited by four lines: Δ₁: x = LB, Δ₂: x = UB, Δ₃: y = LB, and Δ₄: y = UB. As the initial position of Ship A is inside the exploration space, the foremost collision position point C overlaps with the intersection of the half-line of Ship A with the square perimeter. If −90 < α < 90, the intersection of Ship A trajectory with the space exploration perimeter occurs along lines Δ₂, Δ₃, and Δ₄. Conversely, if 90 < α < 270, the intersection could occur along lines Δ₁, Δ₃, or Δ₄. The lines: 1, 2, 3 and 4 of equation (6) define the abscissa of the point related to the intersection of the half-line related to Ship A trajectory with Δ₂, Δ₁, Δ₄, and Δ₃, respectively.

x_{C} = {\begin{cases} U B & i f A \in [L B, U B] \land α \in] - 90, 90 [ \\ L B & i f A \in [L B, U B] \land α \in] 90, 270 [ \\ x_{C u b} & i f x_{C u b} \in [L B, U B] \land α \in] 0, 180 [∖ {90} \\ x_{C l b} & i f x_{C l b} \in [L B, U B] \land α \in] - 180, 0 [∖ {- 90} \end{cases}

(6)

where, A = tan(α) UB + y_A − tan(α) x_A,

\begin{aligned} x_{C u b} & = \frac{U B - y_{A} + t a n (α) x_{A}}{t a n (α)}, a n d \\ x_{C l b} & = \frac{L B - y_{A} + t a n (α) x_{A}}{t a n (α)} . \end{aligned}

If α is 90 or −90, the intersection with the search space border is (x_A,UB) or (x_A,LB), respectively. To find the farthest initial position of Ship B relative to Ship A, we compute the intersection of the half-line from the collision point with the space search border and the half-line delta of the initial positions. The slope returns to the origin of the initial position, equal to β − 180. For example, in Figure 4, point C^′ is the intersection of the square perimeter and Ship A's trajectory.

Figure 4.

Limit of ship B initial position.

Drawing the ray from C^′ with slope β − 180 intersects the ray from A through B at point B^′, the furthest initial position of Ship B leading to a collision. If the intersection is outside the search space, point B^′ is the intersection of the ray from A through B and the square perimeter. Equation (7) describes the intersection at point B^′.

y_{C^{'}} + t a n (β - 180) (x - x_{C^{'}}) = y_{A} + t a n (δ) (x - x_{A})

(7)

As a result, the value of the point B^′ abscissa is provided by equation (8). The first line defines V and δ(V) (the abscissa and ordinate of B^′, respectively) as solutions of equation (7) if its value is within the square boundaries. The second line describes the intersection of the ray δ with square boundaries provided by equation (6), where we replace α by δ. We retain this value if the first line solution is out of the square boundaries.

x_{B^{'}} = {\begin{matrix} V = \frac{y_{A} - t a n (δ) x_{A} - y_{C^{'}} + t a n (β - 180) x_{C^{'}}}{t a n (β - 180) - t a n (δ)} \\ i f L B \leq V, δ (V) \leq U B \\ X_{C} (δ) E q u a t i o n (6) \\ i f V, δ (V) < L B \lor U B < V, δ (V) \end{matrix}

(8)

Therefore, the boundaries of the abscissa of the initial positions of Ship B are between x_A and x_B′. Then, we state that the number of potential initial positions is equal to the distance between the position of Ship A and the point B^′ over the granularity, as described by formula (9).

N_{i n i t P o s} = \frac{\sqrt{{(x_{A} - {x^{'}}_{B})}^{2} + {(y_{A} - {y^{'}}_{B})}^{2}}}{g r a n}

(9)

Since the total number of search space points is equal to ((UB − LB)/gran)², the reduction rate R is equal to one minus the number of potential initial positions of Ship B. Equation (10) provides the formula to compute the reduction rate.

R = 1 - \frac{\sqrt{{(x_{A} - {x^{'}}_{B})}^{2} + {(y_{A} - {y^{'}}_{B})}^{2}} g r a n}{{(U B - L B)}^{2}}

(10)

4.3 Modeling assumptions

The proposed formulation focuses on two-vessel encounters, enabling a pair-wise analysis of potential collision scenarios. This choice is motivated by the need to mitigate the combinatorial explosion inherent in multi-vessel interactions. By decomposing the global problem into pair-wise interactions, the framework prioritizes the most critical vessel pairs, particularly those within short separation distances. These distances are directly related to vessel maneuverability and reaction capabilities, which vary significantly depending on vessel type (e.g., heavy vessels such as tankers may require safety distances on the order of 3 nautical miles, whereas lighter vessels such as small crafts or zodiacs operate within much shorter ranges). This defines an attention zone restricted to distances within which collision avoidance maneuvers must be safely decided and executed. Choosing vessel pairs with high collision likelihood allows one to prune the constraint solving search space and this heuristic in general provide shorter witness traces of CQS situation cases.

The spatial domain is modeled as a bounded planar region, typically defined as a square area (e.g., 5 NM × 5 NM). This representation corresponds to a common discretization approach in maritime navigation models. The size of the domain is directly linked to both the chosen granularity and the dynamic characteristics of the vessels involved, ensuring that the exploration space remains sufficient by size and consistent with physically meaningful interaction ranges.

Furthermore, the current formulation assumes the absence of additional environmental or traffic constraints. While this simplification allows for a tractable geometric analysis based on relative motion (V _r = V _A − V _B ), it can be extended by incorporating structured navigational elements such as Traffic Separation Schemes (TSS), restricted navigation zones, or environmental conditions (e.g., ice fields). These elements can be naturally integrated into the framework through the definition of constrained attention zones geometry, i.e., further refining the admissible configuration space.

Finally, the proposed reduction strategy supports progressive refinement of decision-making processes. The geometric filtering enables rapid identification of critical configurations, which can then be combined with higher-frequency monitoring data (e.g., GNSS updates at 0.5-s intervals Ahmed³³ to support real-time situational awareness and decision support. This multi-layered approach aligns with modern maritime systems that integrate sensing, prediction, and navigation control decision making.

5 Implementation

Determining the relative angle δ between the approaching ships’ speed vectors plays a central role in the collision analysis model. This angle measures the direction of the relative motion of ship A with respect to ship B, based on their respective velocities and heading angles. We use δ to provide the orientation of the relative velocity vector, which is later used in subsequent geometric constructions.

Algorithm 1 describes the procedure for calculating δ using trigonometric projections of both ships’ velocity vectors.

Algorithm 1. Computation of the Relative Angle δ

Input: α, β, Va, Vb

Output: δ

1. α_rad ← radians(α);

2. β_rad ← radians(β);

3. Vr_x ← Va cos(α_rad) - Vb cos(β_rad) ;

4. Vr_y ← Va sin(α_rad) - Vb sin(β_rad);

5. δ ← degrees(arctan2(Vr_y, Vr_x));

6. return δ mod 360;

The algorithm converts the headings α and β into radians, enabling the use of classical trigonometric functions. Each ship's velocity vector is projected onto horizontal and vertical axes, and the relative velocity is obtained by subtracting the components of both vectors. Finally, δ is computed using the arctan2 operator and normalized to ensure numerical stability in downstream geometric computations.

To operationalize the geometric feasibility constraints used later in our model, we extend the implementation with two additional procedures. The first computes point C where the bearing line of ship A intersects the domain boundaries. The second computes the point B^′ on the interception line defined by the angle δ and the heading difference β − δ. These algorithms explicitly integrate domain bounds and orientation constraints, allowing the model to handle variations in ship speed and directional shifts more robustly.

Algorithm 2. Computation of Point C at Boundary Intersection

Algorithm 2 determines the boundary-intersection point by evaluating all geometric cases induced by the quadrant of α. This computation is fundamental for determining the feasible region in which ship A can generate a potential collision course.

Algorithm 3. Computation of Point B′ on the Interception Line

Algorithm 3 computes the interception point B^′ using a slope-intersection formulation derived from the relative motion geometry. If the computed B^′ lies outside domain bounds, the computation defaults to the boundary intersection point previously obtained in Algorithm 2.

6 Evaluations

In this section, we show how the choice of position parameters and speed vectors governs the reduction of the constraint space to identify close-quarters situations between ships. We ran all the experiments on a Dell Laptop with a processor Intel i5-1234U @ 1.3 GHz, 24 GiB memory, and Windows 11 Professional. We have used SWI-Prolog 10.0.2-1 for Microsoft Windows (64 bit) library CLP(FD): Constraint Logic Programming over Finite Domains. The source codes are available on GitHub Geometric optimization maritime project repository Bhb.³⁴ The evaluation is divided into four subsections: the first considers the case where ships move at the same speed, while the second addresses the more general case where ships move at different speeds. Based on the computation time, introduced in the third subsection, we show the complexity and analyze the worst-case computation time in the following subsections.

6.1 Identical-speed navigation scenario

In this first evaluation stage, the reduction rate depends solely on the angular configuration (α,β) and the initial position of Ship A. In Figure 5, the headings of Ship A and Ship B are 60° and 30°, respectively, while the initial position of Ship A is varied.

Figure 5.

Reduction rates with prefixed headings, α = 60°, β = 30°.

Figure 5 illustrates the distribution of reduction rate values, forming an inverted pyramid shape. The bottom region (darker area) corresponds with the lowest reduction rates are around 97%, whereas the top region (brighter area) has the highest reduction rates, which are close to 100%. Given a canvas granularity of 441 points over a 10 × 10 square, the reduction of 97% corresponds to a segment of length 13 representing the initial positions of Ship B. Let C denote the intersection between the circle centered at the initial position of Ship A, located at A = (−10, −1.5), and the left boundary of the canvas. The angle δ formed at vertex A between the side parallel to the x-axis and the segment [AC] is 130°, which matches within acceptable error margin with the theoretical value of 135° predicted by equation (4). This difference can be reduced with finer grain canvas coordinate system.

For this value of δ, the longest segment in the exploration space corresponds to the diagonal from the bottom-right to the top-left corner. Although this configuration would typically suggest a low reduction, it instead yields the highest reduction, as Ship A is close to exiting exploration space. Consequently, all initial positions of Ship B along with this segment do not lead to a collision. From this corner, keeping the y-coordinate of Ship A at its minimum and decreasing its x-coordinate toward 0 reduces the length of the segment with slope δ, while increasing the number of collision-inducing configurations due to the expansion of Ship A's trajectory. As the x-coordinate of Ship A decreases further to −10, the length of the segment with slope δ continues to decrease, as it becomes constrained by the boundaries of the exploration space. This rise and fall in the number of initial positions leading to a collision explains the symmetry of the inverted pyramid.

Figure 6 illustrates the correlation between the courses α and β of the ships and the average reduction rate. The shape displays symmetry with respect to both diagonals of the canvas and shows four minima in the reduction rate, which are around 97.5%. The discretizations of the headings are performed using 50 uniformly distributed points over the interval [0°, 360°].

Figure 6.

Average reduction rates with different headings of ship A and B.

In Figure 6, the regions with the highest reduction rate correspond to Ship A and Ship B traveling in nearly opposite directions or in the same direction. Although moving along diagonals is assumed to yield better results, this assumption is incorrect. As the headings deviate further from the diagonal, the segment lengths decrease sharply, causing an increase in the reduction rates, as seen in the green areas.

Along the diagonal where the values of α and β are symmetric with respect to the 0° axis, the reduction rate remains constant at 97.5%. This behavior arises because the average reduction rate computed for a given pair (α, β) forms a planar distribution rather than a pyramidal one.

This experiment can guide the explorer component in choosing the initial headings of both ships, targeting the minimum reduction rate to maximize the number of configurations to be verified.

6.2 Different-speed navigation scenario

Figure 7 provides a geometric interpretation of the effect of speed asymmetry on the collision constraint segment.

Figure 7.

Effect of speed asymmetry on the collision constraint segment geometry for fixed headings (α,β). (a) Ship A faster than Ship B (V_a = 2V_b), (b) Ship B faster than Ship A (V_b = 2V_a).

When ships move at different speeds, the relative velocity vector becomes dominated by the faster vessel. In the case where Ship A is faster (V_a = 2V_b), illustrated in Figure 7(a), the relative velocity tilts toward Ship A, causing the collision constraint segment to rotate and stretch along its course. As a consequence, the set of initial positions of Ship B that may result in a close-quarters situation expands in the direction of Ship A's trajectory, while shrinking on the opposite side. This deformation highlights the dominant role of the faster vessel in shaping collision-prone configurations.

A complementary inverse configuration is obtained when Ship B is faster than Ship A (V_b = 2V_a), as illustrated in Figure 7(b). In this configuration, the relative velocity vector is oriented toward Ship B, inducing a corresponding rotation and elongation of the collision constraint segment. The admissible collision corridor consequently extends along Ship B's trajectory while contracting in the opposite direction. This inverse dominance scenario confirms that the orientation and extent of the collision constraint segment are primarily governed by the relative velocity vector rather than by absolute vessel headings alone.

Figure 8 shows the speed configuration where V_a = 2V_b, with headings α = 60 and β = 30. For this configuration, δ is equal to 8383. As the abscissa of Ship A decreases from 10 to −10, the length of the segment with slope δ increases, resulting in a lower reduction rate. This behavior reflects a loss of symmetry compared to the case of equal vessel speeds, highlighting the impact of speed and initial position on the symmetry of the reduction rate values. Also, the reduction surface is characterized by a smooth variation and a higher reduction rate, which ranges from 85% to 100%. Since the reduction rate is less significant when vessels travel at different speeds, this supports selecting initial conditions with heterogeneous speeds to generate a wider range of scenarios for verifying whether COLREG rules can effectively prevent collisions.

Figure 8.

Reduction surface for navigation configuration with (α,V_a,β,V_b) = (60°, 20, 30°, 10).

Figure 9 illustrates the correlation between the courses α, β, the speeds V_a = 20, V_b = 10 of the ships and the average reduction rate.

Figure 9.

Average reduction rates with different headings of ship A and B when V_a = 20 and V_b = 10.

In contrast to the identical-speed navigation scenario, the diagonal corresponding to the equation α = 360 − β disappears. This diagonal represents a sailing configuration in which the ships’ headings are opposite. The initial positions of Ship A, Ship B, and the collision point define an isosceles triangle, where the base corresponds to the initial positions of Ship B that lead to encounter situations. When both ships have identical speeds, this geometric symmetry is preserved. As the speed difference between the ships increases, the symmetry is progressively broken, and the triangle deforms into a scalene configuration. This deformation results in a stretching of the base, which leads to lower reduction rates.

An additional observation specific to Version 2 concerns the behavior of the symmetric corners with respect to the yellow diagonal. In fact, when α = 360 and β = 0, the ships are sailing along the same heading, which corresponds to the scenario represented by the yellow diagonal. A similar situation occurs when α = 0 and β = 360. As the configuration moves farther away from these corner cases, the geometric similarity with the yellow diagonal decreases. Consequently, the alignment of the ships’ headings becomes less favorable, and the effectiveness of the reduction progressively diminishes.

Figure 8 illustrates a sharp reduction rate along the diagonal for which α = β. When both vessels maintain identical headings, the encounter corresponds to an overtaking configuration. If the faster vessel is located ahead of the slower one, collision scenarios are excluded, yielding a reduction rate of 100%. Conversely, when the faster vessel is initially positioned astern, the occurrence of a collision is governed by the relative speed and the inter-vessel distance, considered with respect to the remaining trajectory within the canvas. In this case, the reduction rate is necessarily below 100%. This alternation between overtaking configurations accounts for the spikes observed at the maximum values of the reduction rate.

If the speed of Ship A increases, the maximum reduction along diagonal progressively decreases. This decrease in the reduction rate can be attributed to the fact that, at higher speeds, a trailing vessel encounters a greater set of conditions under which a collision with the slower vessel may occur while both vessels sail in the same direction. Furthermore, the reduction surface exhibits an increasingly flat profile. This trend indicates that higher speed ratios correspond to an increased number of initial positions leading to collision scenarios. This behavior is reflected in Figure 7(a). As the initial positions of Ship B align with the direction of the faster vessel, the length of the corresponding segment exceeds that obtained when both vessels travel at identical speeds.

When selecting vessel speeds, the experiment can be run to guide the explorer component in determining the initial headings of both ships, with the objective of minimizing the reduction rate and thereby maximizing the number of configurations available for verification.

6.3 Computation time (performance)

This section evaluates both the computational performance and the algorithmic complexity of the proposed geometric reduction framework. In addition to reducing the search space, it is essential to assess the scalability of the method when applied exhaustively over the parameter domain.

We measure the execution time required to compute the average reduction rate R over all heading combinations (α,β). The headings are uniformly sampled over [0°, 360°] using 50 discrete values per variable, resulting in 2500 combinations. For each pair (α,β), the reduction is evaluated over a grid of 441 positions corresponding to the domain [LB,UB]² = [−10,10]².

The results in Table 1 show that the full evaluation is completed in approximately 140 s, with an average cost of 55.44 ms per heading pair. This confirms that the proposed analytical approach remains computationally efficient even under exhaustive exploration.

6.4 Complexity analysis

From an algorithmic perspective, the computational complexity of the proposed method can be expressed as follows.

Let N_α and N_β denote the number of sampled heading values, and let N_p denote the number of grid positions for Ship A. The overall complexity of the evaluation process is:

O (N_{α} \cdot N_{β} \cdot N_{p})

(11)

In the current implementation:

N_{α} = N_{β} = 50, N_{p} = 441

which yields:

O (50 \times 50 \times 441) = O (10^{6})

operations.

Each inner computation consists of a constant number of arithmetic and trigonometric operations, implying O(1) per grid point. Therefore, the total complexity scales linearly with respect to both the number of heading samples and the spatial resolution of the domain.

This linear scalability is a key advantage of the proposed method. Unlike simulation-based approaches, which may involve iterative trajectory integration, the present framework relies on closed-form geometric computations, ensuring predictable and efficient performance.

6.5 Worst-case timing analysis

To further analyze performance variability, Table 2 reports the ten slowest heading configurations observed during the evaluation.

Table 1.
Computational performance of the search-space reduction model.

Parameter Value

Heading samples per variable 50

Total (α, β) combinations 2500

Grid size per combination 441 positions

Total execution time (s) 140.14

Average time per combination (ms) 55.44

Minimum time per combination (ms) 0.00

Maximum time per combination (ms) 351.00

Parameter	Value
Heading samples per variable	50
Total (α, β) combinations	2500
Grid size per combination	441 positions
Total execution time (s)	140.14
Average time per combination (ms)	55.44
Minimum time per combination (ms)	0.00
Maximum time per combination (ms)	351.00

Table 2.

Top 10 slowest (α,β) configurations.

Rank	α (deg)	β (deg)	R	Time (ms)
1	14.69	117.55	89.52	351.00
2	14.69	110.20	89.64	332.98
3	14.69	36.73	93.82	324.07
4	14.69	124.90	89.40	274.43
5	14.69	95.51	89.85	260.22
6	14.69	102.86	89.74	254.18
7	14.69	132.24	89.29	219.21
8	183.67	44.08	88.56	213.79
9	14.69	168.98	88.47	201.32
10	14.69	176.33	88.40	200.33

The worst-case execution times remain below 0.4 s, confirming the robustness of the method. These higher runtimes are associated with geometrically complex configurations, where line intersections approach domain boundaries or where slope differences become small, increasing numerical sensitivity.

Despite these localized increases, the overall runtime distribution remains stable, ensuring predictable performance across the parameter space.

Overall, the evaluation demonstrates that the proposed method achieves significant search-space reduction while maintaining low computational overhead and linear scalability, making it suitable for large-scale parametric analysis and integration into constraint-based verification frameworks.

The assumption of constant vessel speeds and headings over short time intervals is supported by the computational performance of the proposed framework. Based on the worst-case timing analysis, the maximum computation time per configuration remains below 0.35 s, which is significantly shorter than the time scale over which meaningful changes in vessel dynamics or environmental conditions occur (c. f. Modeling Assumptions).

In practical maritime scenarios, vessel maneuvers such as heading changes or speed adjustments typically evolve over several seconds to minutes due to inertia and steering system latency. Therefore, within the considered computation window, vessel motion can be reasonably approximated as uniform, corresponding to a constant average speed assumption during discrete time steps (t₁,t₂,…,t_n).

This time-scale separation ensures that the verification process operates faster than the underlying physical evolution of the system, enabling near real-time detection of collision-prone configurations. Moreover, the assumption of constant speeds and headings allows the derivation of closed-form geometric constraints, which are essential for enabling analytical pruning of the search space. Without this assumption, the problem would require time-dependent trajectory integration, significantly increasing computational complexity.

Finally, even in the presence of small variations in speed or heading, the resulting geometric constraints remain locally valid, ensuring that the reduction strategy is robust to minor deviations from ideal motion assumptions.

7 Threats to result validity

The motivation for this work stems from the use of Constraint Logic Programming (CLP) to encode MASS navigation rules together with their contextual constraints (incl. COLREG compliance) in an explainable and verifiable framework. While solving such constraint systems can rapidly become computationally demanding, our results demonstrate that decomposing complex navigation scenarios into tractable use cases and incorporating context-dependent feasibility constraints can substantially reduce verification complexity.

The main contribution of this work is the derivation of application-specific feasibility constraints based on the geometric properties of vessel placement. These constraints enable the elimination of nearly 90% of noncritical configurations as spurious from the point of view of verification. This pruning of the search space allows constraint solver to be focused on the remaining 10% of scenarios that may lead to close-quarters situations.

Overall, these findings show that feasibility-based filtering provides an effective means of significantly reducing the verification search space, thereby enhancing the scalability of formal reasoning approaches for practical maritime safety analysis.

Although feasibility constraints yield significant reductions, the intrinsic complexity of real-world maritime encounter scenarios remains only partially characterized. Even seemingly simple configurations, such as two-vessel encounters that do not strictly adhere to traffic separation schemes, can give rise to highly irregular and nonlinear feasibility boundaries when hazardous zones overlap. In such cases, constraint solvers may yield solutions that are theoretically valid but difficult to interpret operationally, especially when physical plausibility is uncertain or when small positional variations lead to significant changes in the solution space.

The performance of the proposed approach is also strongly influenced by the structure of the constraints themselves. When geometric assumptions such as symmetric motion, constant speeds, or stable headings are satisfied, the proposed reduction strategy remains highly effective. However, as encounter parameters become increasingly coupled or evolve asymmetrically, the effectiveness of constraint-based pruning diminishes and may no longer yield sufficient reductions of the search space. This is particularly evident in dynamic or congested waterways, where interactions among vessels create inter-dependencies that are not yet captured by our current constraint models.

Although the proposed method eliminates a substantial portion of non-critical (spurious) configurations, those which exclude CQS and can be pruned from CSP search space, its applicability remains conditioned by the domain specific simplifying assumptions inherent in geometric and kinematic modeling.

In real operational contexts, factors such as human decision-making biases, environmental disturbances, and cyber-induced perturbations may modify the feasibility landscape in ways that are not captured by the present framework. Extending the geometric optimization with follow-up refinement with realistic simulation conditions using Open Simulation Platform OpenSim³⁵ has been proposed in Lahbib et al.³² and therefore is out of the scope of this study.

However, the computational complexity of multi-vessel interactions is still not fully understood, and the occurrence of nonphysical or degenerate constraint solutions indicates the need for additional semantic filtering mechanisms.

These limitations emphasize that, while constraint-based reasoning significantly enhances tractability, it does not yet fully cover the operational complexity of maritime navigation. Future research should focus on systematically characterizing the evolution of constraint structures in more realistic scenarios and on integrating richer contextual information to mitigate misleading or overly idealized solutions.

The presence of additional navigational structures, such as complicated Traffic Separation Schemes, coastal routing corridors influenced by tides, and static or dynamic obstacles, further limits the applicability of the proposed approach. These elements introduce extra geometric and regulatory constraints that can interact in complex, nonlinear ways with collision-avoidance rules. When such contextual constraints are combined with the basic encounter geometry, the resulting feasible regions may break into smaller parts or become strongly asymmetric, which reduces the effectiveness of pruning and makes solver results harder to interpret. This illustrates that the constraint system can change significantly as new contextual elements, such as lane boundaries or restricted navigation areas, are introduced, and that formal reasoning approaches must take these interactions into account to remain operationally relevant.

8 Conclusion and future work

In summary, this study shows that the combination of constraint logic programming and geometric feasibility constraints provides an effective means of addressing the complexity of safety verification in MASS navigation rules. Beyond validating the proposed approach, the results illustrate how context-aware constraints can assist both researchers and practitioners by helping to focus simulations and verification efforts on the most relevant initial conditions.

Future work will aim to extend the set of feasibility constraints to include additional parameters that are often neglected in quantitative navigation models. In particular, we plan to consider factors such as human decisionmaking biases and potential cyber threats, which are widely recognized as contributors to maritime incidents. We also intend to investigate whether inter-dependencies between situational parameters can give rise to new forms of constraints that further reduce the computational search space and improve analytical efficiency. As for optimization approach, we consider nature-inspired and meta-heuristic optimization algorithms such as harmony search algorithm Siddique and Adeli³⁶ and simulated annealing Siddique and Adeli³⁷ as alternative approaches.

Building on our previous work that integrates CLP with model-based simulation for COLREG-compliant path generation Lahbib et al.,³² we plan to exploit entire set of the refined modeling features of the Open Simulation Platform (OSP) accessible via our framework. This integration is expected to enhance interoperability, realism, and computational efficiency in future maritime navigation analysis tools.

Finally, the solution was implemented with the perspective of possible integration with the autonomous vessel onboard navigation system provided by MindChip AS Mõlder et al.³⁸ including practical end-to-end verification in realworld situations. Also, our future work is to connect with a training simulator, such as Wartsï la NTPRÖ 7, to provide trainees with critical scenarios.

Footnotes

Ethical approval

Funding

This research was partially supported by ErasmusPlus Credit Mobility Taltech-UTM (2025).

Declaration of conflicting interests

The authors declared no potential conflicts of interest with respect to the research, authorship, and/or publication of this article.

ORCID iD

Jüri Vain

References

Estevez

Lopez-Guede

Valle-Echavarri

, et al. Enhanced dynamic obstacle avoidance for linked multi-agent systems by an extended hybrid reciprocal velocity obstacle model. Integr Comput Aided Eng 2026; 33: 24–37.

Grosset

Fougeres

A-J

Djoko-Kouam

, et al. Multi- agent simulation of autonomous industrial vehicle fleets: towards dynamic task allocation in V2X cooperation mode. Integr Comput Aided Eng 2024; 31: 249–266.

Tavaris

Scandino

Luca Foresti

, et al. A cost-effective autonomous underwater system for small size object detection. Integr Comput Aided Eng 2025; 32: 258–271.

Liu

Rong

Neri

, et al. Deep deterministic policy gradient with constraints for gait optimisation of biped robots. Integr Comput Aided Eng 2024; 31: 139–156.

Vain

Tsiopoulos

Walden

, et al. Constraint´ programming-based verification of COLREG safety. IEEE J Oceanic Eng 2025; 50: 2797–2821.

Reif

. Complexity of the mover’s problem and generalizations. J ACM 1979; 26: 682–694.

Lahbib

Bennani

Vain

. Autonomous vessels collision verification: geometric optimization. In: IFIP international conference on artificial intelligence applications and innovations, 2025, pp.132–145: Springer.

Hanus

Sacerdoti Coen

. Functional and constraint logic programming. Springer, 2021.

Refalo

. Impact-based search strategies for constraint programming. In: CP 2004, 2004, pp.557–571: Springer.

10.

Cicirello

Smith

. Heuristic selection for stochastic search optimization. In: CP 2004, 2004, pp.197–211.

11.

Pretschner

. Classical search strategies for test case generation with Constraint Logic Programming. In: FATES’01, 2001.

12.

Boizumault

Delon

Peridy

. Constraint logic programming for examination timetabling. J Log Program 1996; 26: 217–233.

13.

Papadimitriou

. The Euclidean travelling salesman problem is NP-complete. Theor Comput Sci 1977; 4: 237–244.

14.

Bertagnon

Gavanelli

. Improved filtering for the Euclidean TSP in CLP(FD). Proc AAAI Conf Artif Intell 2020; 34: 1412–1419.

15.

Graham

. An efficient algorithm for determining the convex hull of a finite planar set. Inf Process Lett 1972; 1: 132–133.

16.

Bellodi

Bertagnon

Gavanelli

, et al. Improving Euclidean TSP solving with predicted nocrossing constraints. In: AIxIA 2020, 2021, pp.318–334.

17.

Naeem

Rajabally

, et al. COLREGs-compliant path planning for autonomous surface vehicles. IFAC-PapersOnLine 2017; 50: 13662–13667.

18.

Pedersen

Vasanthan

Karolius

, et al. Generating structured encounters for verifying automated collision and grounding avoidance systems. J Phys: Conf Ser 2023; 2618: 012013.

19.

Fiorini

Shiller

. Motion planning in dynamic environments using velocity obstacles. Int J Rob Res 1998; 17: 760–772.

20.

Tam

Bucknall

Greig

. Review of collision avoidance and path planning methods for ships in close range encounters. J Navig 2009; 62: 455–476.

21.

Krasowski

Althoff

. Temporal logic formalization of marine traffic rules. In: Proceedings of IEEE intelligent vehicles symposium, 2021, pp.186–192.

22.

Shokri-Manninen

Vain

Walden

. Formal verification of COLREG-based navigation of maritime autonomous systems. In: Proceedings of 18th international conference on software engineering and formal methods, 2020, pp.41–59.

23.

Wen

, et al. Safety-assured decision support for ASV navigation via hybrid graph planning and timed automata verification. Expert Syst Appl 2026; 312: 131367. ISSN 0957-4174.

24.

Miao

Amam

Slaets

, et al. An improved real-time collision-avoidance algorithm based on hybrid A* in a multi-object-encountering scenario for autonomous surface vessels. Ocean Eng 2022; 255: 111406. ISSN 0029-8018.

25.

International Maritime Organization. Convention on the international regulations for preventing collisions at sea (COLREGs). IMO Publication, 2003.

26.

Eriksen

BOH

Bitar

Breivik

, et al. Hybrid collision avoidance for ASVs compliant with COLREGs rules 8 and 13–17. Front Robot AI 2020; 7: 11.

27.

Marriott

Stuckey

Wallace

. Constraint Logic Programming. In: Handbook of constraint programming. Elsevier, 2006, pp.409–452.

28.

Popescu

Erdeniz

Felfernig

, et al. An overview of machine learning techniques in constraint solving. J Intell Inf Syst 2022; 58: 91–118.

29.

Van Roy

. Programming paradigms for dummies. In: New computational paradigms for computer music. Ircam/Delatour, 2009, pp.9–47.

30.

Triska

. Correctness considerations in CLP(FD) systems . PhD Thesis, Technische Universitat Wien, 2013.

31.

Triska

. A9 library(clpfd): CLP(FD): constraint logic programming over finite domains, https://www.swiprolog.org/man/clpfd.html.

32.

Lahbib

Vain

Taha Bennani

, et al. Two-phase path planning for fuel-efficient safe navigation. In: 5th European workshop on maritime systems resilience and security 2025 (MARESEC 2025), 2025, Rostock, Germany. DOI: 10.5281/zenodo.17120607.

33.

Ahmed

. Optimizing GNSS data sampling rates for improving precise point positioning accuracy and reducing convergence time. Cihan Univ-Erbil Sci J 2025; 9: 36–40.

34.

Lahbib

. Geometric optimization maritime, https://github.com/hibabhb/Geometric-optimization-maritime (2026).

35.

Evang

, et al. Open Simulation Platform, https://opensimulationplatform.com/ (May 2026).

36.

Siddique

Adeli

. Harmony search algorithm and its variants. Int J Pattern Recognit Artif Intell 2015; 29: 1539001.

37.

Siddique

Adeli

. Simulated annealing, its variants and engineering applications. Int J Artif Intell Tools 2016; 25: 1630001.

38.

Mõlder

Janson

Vain

, et al. Integrated path planning of MASS navigation in non-standard maritime encounters. In: The 20th annual IEEE international systems conference (SysCon 2026), Halifax, Canada, 6–9 April 2026, Conference Proceedings. Ed. Orr, Brianna. IEEE.