research-article

Symbolic calculation of k-shortest paths and related measures with the stochastic process algebra tool CASPA

Authors:

Michael Günther,

Johann Schuster,

Markus SiegleAuthors Info & Claims

DYADEM-FTS '10: Proceedings of the First Workshop on DYnamic Aspects in DEpendability Models for Fault-Tolerant Systems

Pages 13 - 18

https://doi.org/10.1145/1772630.1772635

Published: 27 April 2010 Publication History

Get Access

Abstract

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.

References

[1]

J. Azevedo, J. Madeira, E. Martins, and F. Pires. A Shortest Paths Ranking Algorithm. In Proc. of the Annual Conference AIRO'90 Operational Research Society of Italy, pages 1001--1011, IEEE, 1990.

Google Scholar

[2]

J. Bachmann, M. Riedl, J. Schuster, and M. Siegle. An Efficient Symbolic Elimination Algorithm for the Stochastic Process Algebra tool CASPA. In SOFSEM 2009: Theory and Practice of Computer Science, pages 485--496, Špindlerův Mlýn, Czech Republic, 2009. Springer, LNCS 5404.

Digital Library

Google Scholar

[3]

M. Bouissou and J.-L. Bon. A new formalism that combines advantages of fault-trees and Markov models: Boolean logic driven Markov processes. Reliability Engineering and System Safety, 82:149--163, 2003.

Crossref

Google Scholar

[4]

CUDD website. http://vlsi.colorado.edu/~fabio/CUDD/, (last checked March 2010).

Google Scholar

[5]

M. Günther. Pfadbasierte Algorithmen zur Zuverlässigkeitsanalyse. Master's thesis, Univ. der Bundeswehr München, Fakultät für Informatik (in German), 2009.

Google Scholar

[6]

M. Kuntz, M. Siegle, and E. Werner. Symbolic Performance and Dependability Evaluation with the Tool CASPA. In Europ. Perf. Engineering Workshop, pages 293--307. LNCS 3236, 2004.

Google Scholar

[7]

W. Schmid. Berechnung kürzester Wege in Straßennetzen mit Wegeverboten. PhD thesis, Universität Stuttgart, Fakultät für Bauingenieur- und Vermessungswesen, 2000.

Google Scholar

[8]

M. Siegle. Behaviour analysis of communication systems: Compositional modelling, compact representation and analysis of performability properties. Shaker Verlag, Aachen, 2002.

Google Scholar

[9]

M. Walter, M. Siegle, and A. Bode. OpenSESAME: The Simple but Extensive, Structured Availability Modeling Environment. Reliability Engineering and System Safety, 93(6):857--873, 2007.

Crossref

Google Scholar

[10]

E. Werner. Leistungsbewertung mit Multi-terminalen Binären Entscheidungsdiagrammen. Master's thesis, Univ. Erlangen, Computer Science 7 (in German), 2003.

Google Scholar

Cited By

View all

Nguyễn TReyes RBauschert T(2022)Multi-step migration of optical connections to minimize disruption time in flex-grid networksJournal of Optical Communications and Networking10.1364/JOCN.46370214:10(866)Online publication date: 27-Sep-2022
https://doi.org/10.1364/JOCN.463702
Khai NReyes RBauschert T(2022)Multi-step Migration of Optical Connections in Flex-grid Networks to Minimize Disruption TimeICC 2022 - IEEE International Conference on Communications10.1109/ICC45855.2022.9838740(5725-5730)Online publication date: 16-May-2022
https://doi.org/10.1109/ICC45855.2022.9838740
Ábrahám EBecker BDehnert CJansen NKatoen JWimmer R(2014)Counterexample Generation for Discrete-Time Markov ModelsAdvanced Lectures of the 14th International School on Formal Methods for Executable Software Models - Volume 848310.1007/978-3-319-07317-0_3(65-121)Online publication date: 16-Jun-2014
https://dl.acm.org/doi/10.1007/978-3-319-07317-0_3
Show More Cited By

Recommendations

An Efficient Symbolic Elimination Algorithm for the Stochastic Process Algebra Tool CASPA
SOFSEM '09: Proceedings of the 35th Conference on Current Trends in Theory and Practice of Computer Science

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 ...
Dependability modelling with the stochastic process algebra tool CASPA
DYADEM-FTS '10: Proceedings of the First Workshop on DYnamic Aspects in DEpendability Models for Fault-Tolerant Systems

This note describes CASPA, a stochastic process algebra tool for performance and dependability modelling, analysis and verification. Internally, the tool works with the symbolic data structure MTBDD (multi-terminal binary decision diagram), which allows ...
Near-shortest and K-shortest simple paths

We present a new algorithm for enumerating all near-shortest simple (loopless) s-t paths in a graph G = (V, E) with nonnegative edge lengths. Letting n = |V| and m = |E|, the time per path enumerated is O(nS(n, m)) given a user-selected shortest-path ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

DYADEM-FTS '10: Proceedings of the First Workshop on DYnamic Aspects in DEpendability Models for Fault-Tolerant Systems

April 2010

45 pages

ISBN:9781605589169

DOI:10.1145/1772630

Conference Chair:
Arndt Bode
Technische Universitát Múnchen

Permission to make digital or hard copies of all or part of this work for personal or classroom use is granted without fee provided that copies are not made or distributed for profit or commercial advantage and that copies bear this notice and the full citation on the first page. Copyrights for components of this work owned by others than ACM must be honored. Abstracting with credit is permitted. To copy otherwise, or republish, to post on servers or to redistribute to lists, requires prior specific permission and/or a fee. Request permissions from [email protected]

In-Cooperation

IEEE Computer Society TC on Dependable Computing and Fault Tolerance
IFIP Working Group 10.4 Dependable Computing and Fault Tolerance
EWICS TC7 on Safety, Reliability and Security

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 27 April 2010

Permissions

Request permissions for this article.

Request Permissions

Check for updates

Author Tags

Qualifiers

Research-article

Conference

EDCC '10

Sponsor:

EDCC '10: European Dependable Computing Conference

April 27, 2010

Valencia, Spain

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

7
Total Citations
View Citations
135
Total Downloads

Downloads (Last 12 months)11
Downloads (Last 6 weeks)0

Reflects downloads up to 27 Nov 2024

Other Metrics

View Author Metrics

Citations

Cited By

View all

Nguyễn TReyes RBauschert T(2022)Multi-step migration of optical connections to minimize disruption time in flex-grid networksJournal of Optical Communications and Networking10.1364/JOCN.46370214:10(866)Online publication date: 27-Sep-2022
https://doi.org/10.1364/JOCN.463702
Khai NReyes RBauschert T(2022)Multi-step Migration of Optical Connections in Flex-grid Networks to Minimize Disruption TimeICC 2022 - IEEE International Conference on Communications10.1109/ICC45855.2022.9838740(5725-5730)Online publication date: 16-May-2022
https://doi.org/10.1109/ICC45855.2022.9838740
Ábrahám EBecker BDehnert CJansen NKatoen JWimmer R(2014)Counterexample Generation for Discrete-Time Markov ModelsAdvanced Lectures of the 14th International School on Formal Methods for Executable Software Models - Volume 848310.1007/978-3-319-07317-0_3(65-121)Online publication date: 16-Jun-2014
https://dl.acm.org/doi/10.1007/978-3-319-07317-0_3
Jansen NÁbrahám EZajzon BWimmer RSchuster JKatoen JBecker B(2013)Symbolic Counterexample Generation for Discrete-Time Markov ChainsFormal Aspects of Component Software10.1007/978-3-642-35861-6_9(134-151)Online publication date: 2013
https://doi.org/10.1007/978-3-642-35861-6_9
Wimmer RJansen NÁbrahám EBecker BKatoen J(2012)Minimal critical subsystems for discrete-time markov modelsProceedings of the 18th international conference on Tools and Algorithms for the Construction and Analysis of Systems10.1007/978-3-642-28756-5_21(299-314)Online publication date: 24-Mar-2012
https://dl.acm.org/doi/10.1007/978-3-642-28756-5_21
Braitling BWimmer RBecker BJansen NÁbrahám E(2011)Counterexample generation for Markov chains using SMT-based bounded model checkingProceedings of the joint 13th IFIP WG 6.1 and 30th IFIP WG 6.1 international conference on Formal techniques for distributed systems10.5555/2022067.2022072(75-89)Online publication date: 6-Jun-2011
https://dl.acm.org/doi/10.5555/2022067.2022072
Braitling BWimmer RBecker BJansen NÁbrahám E(2011)Counterexample Generation for Markov Chains Using SMT-Based Bounded Model CheckingFormal Techniques for Distributed Systems10.1007/978-3-642-21461-5_5(75-89)Online publication date: 2011
https://doi.org/10.1007/978-3-642-21461-5_5

View Options

Login options

Check if you have access through your login credentials or your institution to get full access on this article.

Cited By

Recommendations

An Efficient Symbolic Elimination Algorithm for the Stochastic Process Algebra Tool CASPA

Dependability modelling with the stochastic process algebra tool CASPA

Near-shortest and K-shortest simple paths