The Constrained Shortest Path Problem: A Case Study in Using ASMs

dc.creatorStrötmann,Karl
dc.date1997
dc.date.accessioned2024-02-06T12:48:46Z
dc.date.available2024-02-06T12:48:46Z
dc.descriptionThis 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.
dc.formattext/html
dc.identifierhttps://doi.org/10.3217/jucs-003-04-0304
dc.identifierhttps://lib.jucs.org/article/27350/
dc.identifier.urihttps://openrepository.mephi.ru/handle/123456789/7140
dc.languageen
dc.publisherJournal of Universal Computer Science
dc.relationinfo:eu-repo/semantics/altIdentifier/eissn/0948-6968
dc.relationinfo:eu-repo/semantics/altIdentifier/pissn/0948-695X
dc.rightsinfo:eu-repo/semantics/openAccess
dc.rightsJ.UCS License
dc.sourceJUCS - Journal of Universal Computer Science 3(4): 304-319
dc.subjectabstract state machine
dc.subjectsoftware verification
dc.subjectshortest path problem
dc.subjectconstrained shortest path problem
dc.titleThe Constrained Shortest Path Problem: A Case Study in Using ASMs
dc.typeResearch Article
Файлы