Result Verification for Computational Problems in Geodesy

Abstract

The subject of the paper is to present verified methods to solve three important geodetic problems: The Direct and Inverse Problem of geodetic surveying and the three-dimensional resection problem, often also designated as the main problem of Photogrammetry.

The Direct Problem reads as follows: Given a point p on a rotational ellipsoid E, a direction tangential to E and a distance, determine the point q which is reached after “walking” the given distance along a geodesic on E, starting at p in the given direction, and compute the direction of the geodesic in q.

In the Inverse Problem there are given two points p,q on E, and one has to compute the length of a geodesic on E connecting p and q as well as its directions in p and q.

It is shown that the Direct Problem can be treated as an ordinary initial value problem with verified solvers like AWA.

The inverse problem is much more complicated because no characteristic quantity of the geodesic is known. In fact it is an ordinary open boundary value problem and the question whether it is uniquely sovable must be treated. It is shown how to compute an enclosure of the direction of the geodesic in one point. By the aid of this enclosure the problem can be solved by a verified shooting technique using again solvers like AWA.

The three-dimensional resection problem can be reduced to the problem to find the set S of all real positive s ₁, s ₂, s ₃ satisfying the equations

$s^2_2 + s^2_3 - 2_{{s_2}{s_2}{c_1}} = a^2_1$

$s^2_3 + s^2_1 - 2_{{s_3}{s_1}{c_2}} = a^2_2$

$s^2_1 + s^2_2 - 2_{{s_1}{s_2}{c_3}} = a^2_3$

where c _i , a _i , i=1,2,3, are real parameters restricted by the inequalities -1 < c _i < 1, i=1,2,3, $1 - c^2_1 - c^2_2 - c^2_3 + 2_{{c_1}{c_2}{c_3}} \geq 0$, a _i >0, i=1,2,3, a ₁+a ₂>a ₃, a ₂+a ₃>a ₁, a ₃+a ₁>a ₂.

There are discussed three approaches for constructing algorithms for computing narrow inclusions of S. In the first one the fact is used that an initial box containing S can be easily derived. Consequently standard modules like GlobSol or nlss can be applied to achieve the goal.

The idea of the second approach is to construct verifying versions of algorithms for computing S wich are used in practice. However, it turns out that there are instabilities in the resulting methods which are not present in the methods resulting from the first approach.

The aim of the third approach is to derive sufficiently narrow inclusions of S from sufficiently narrow inclusions of all zeros of at most four simple functions of one variable. At the moment experiences with several practical and artificial examples indicate that the third approach is best.