The Constrained Shortest Path Problem: A Case Study in Using ASMs
Karl Strötmann (Siemens AG, Germany)
Abstract: This paper addresses the correctness problem of an algorithm solving the constrained shortest path problem. We define an abstract, nondeterministic form of the algorithm and prove its correctness from a few simple axioms. We then define a sequence of natural refinements which can be proved to be correct and lead from the abstract algorithm to an efficient implementation due to Ulrich Lauther [Lauther 1996] and based on [Desrosiers et al. 1995]. Along the way, we also show that the abstract algorithm can be regarded as a natural extension of Moore s algorithm [Moore 1957] for solving the shortest path problem.
Keywords: abstract state machine, constrained shortest path problem, shortest path problem, software verification
Categories: D.2.4, F.3.1, G.2.2