Symbolic calculation of k-shortest paths and related measures with the stochastic process algebra tool CASPA
Michael F. Gunther, Johann Schuster, Markus Siegle · 2010
CASPA is a stochastic process algebra tool for performance and dependability modelling, analysis and verification. It is based entirely on the symbolic data structure MTBDD (multi-terminal binary decision diagram) which enables the tool to handle models with very large state space. This paper describes an extension of CASPA's solving engine for path-based analysis. We present a symbolic variant of the k-shortest-path algorithm of Azevedo, which works in conjunction with a symbolic variant of Dijkstra's shortest path algorithm. A non-trivial case study illustrates the use of this kind of path-based analysis.