On the Minimisation of Acyclic Models | SpringerLink
Skip to main content
Springer Nature Link
Log in

On the Minimisation of Acyclic Models

  • Conference paper
CONCUR 2008 - Concurrency Theory (CONCUR 2008)

Part of the book series: Lecture Notes in Computer Science ((LNTCS,volume 5201))

Included in the following conference series:

Abstract

This paper presents a novel algorithm to compute weak bisimulation quotients for finite acyclic models. It is developed in the setting of interactive Markov chains, a model overarching both labelled transition systems and continuous-time Markov chains. This model has lately been used to give an acyclic compositional semantics to dynamic fault trees, a reliability modelling formalism.

While the theoretical complexity does not change substantially, the algorithm performs very well in practice, almost linear in the size of the input model. We use a number of case studies to show that it is vastly more efficient than the standard bisimulation minimisation algorithms. In particular we show the effectiveness in the analysis of dynamic fault trees.

This work is supported by the DFG as part of the Transregional Collaborative Research Center SFB/TR 14 AVACS and by the European Commission under the IST framework 7 project QUASIMODO.

This is a preview of subscription content, log in via an institution to check access.

Access this chapter

Log in via an institution

Institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

Similar content being viewed by others

References

  1. Blom, S., Fokkink, W., Groote, J.F., van Langevelde, I., Lisser, B., van de Pol, J.: μcrl: A toolset for analysing algebraic specifications. In: Berry, G., Comon, H., Finkel, A. (eds.) CAV 2001. LNCS, vol. 2102, pp. 250–254. Springer, Heidelberg (2001)

    Google Scholar 

  2. Blom, S., Orzan, S.: Distributed branching bisimulation reduction of state spaces. Electr. Notes Theor. Comput. Sci. 89(1) (2003)

    Google Scholar 

  3. Böde, E., Herbstritt, M., Hermanns, H., Johr, S., Peikenkamp, T., Pulungan, R., Wimmer, R., Becker, B.: Compositional performability evaluation for statemate. In: QEST, pp. 167–178 (2006)

    Google Scholar 

  4. Boudali, H., Crouzen, P., Stoelinga, M.: A compositional semantics for dynamic fault trees in input/output interactive markov chains. In: ATVA, pp. 441–456 (2007)

    Google Scholar 

  5. Bravetti, M.: Revisiting interactive markov chains. Electronic Notes in Theoretical Computer Science 68(5) (2002)

    Google Scholar 

  6. Coppersmith, D., Winograd, S.: Matrix multiplication via arithmetic progressions. In: ACM Symposium on Theory of Computing (1987)

    Google Scholar 

  7. Coste, N., Garavel, H., Hermanns, H., Hersemeule, R., Thonnart, Y., Zidouni, M.: Quantitative evaluation in embedded system design: Validation of multiprocessor multithreaded architectures. In: DATE (2008)

    Google Scholar 

  8. Crouzen, P., Hermanns, H., Zhang, L.: No Cycling? Go Faster! On the minimization of acyclic models. Reports of SFB/TR 14 AVACS 41, SFB/TR 14 AVACS (July 2008), http://www.avacs.org ISSN: 1860-9821

  9. Dovier, A., Piazza, C., Policriti, A.: A fast bisimulation algorithm. In: Berry, G., Comon, H., Finkel, A. (eds.) CAV 2001. LNCS, vol. 2102, pp. 79–90. Springer, Heidelberg (2001)

    Google Scholar 

  10. Dugan, J., Bavuso, S., Boyd, M.: Dynamic fault-tree models for fault-tolerant computer systems. IEEE Transactions on Reliability 41(3), 363–377 (1992)

    Article  MATH  Google Scholar 

  11. Fokkink, W., Pang, J., van de Pol, J.: Cones and foci: A mechanical framework for protocol verification. Formal Methods in System Design 29(1), 1–31 (2006)

    Article  MATH  Google Scholar 

  12. Garavel, H., Lang, F., Mateescu, R., Serwe, W.: Cadp 2006: A toolbox for the construction and analysis of distributed processes. In: CAV (2006)

    Google Scholar 

  13. Goralcikova, A., Koubek, V.: A reduct-and-closure algorithm for graphs. Mathematical Foundations of Computer Science 74, 301–307 (1979)

    MathSciNet  Google Scholar 

  14. Griffioen, W.O.D., Vaandrager, F.W.: A theory of normed simulations. ACM Trans. Comput. Log. 5(4), 577–610 (2004)

    Article  MathSciNet  Google Scholar 

  15. Groote, J.F., Vaandrager, F.: An efficient algorithm for branching bisimulation and stuttering equivalence. In: Paterson, M. (ed.) ICALP 1990. LNCS, vol. 443. Springer, Heidelberg (1990)

    Chapter  Google Scholar 

  16. Hermanns, H.: Interactive Markov Chains: The Quest for Quantified Quality. LNCS, vol. 2428. Springer, Heidelberg (2002)

    MATH  Google Scholar 

  17. Katoen, J.-P., Kemna, T., Zapreev, I.S., Jansen, D.N.: Bisimulation minimisation mostly speeds up probabilistic model checking. In: Grumberg, O., Huth, M. (eds.) TACAS 2007. LNCS, vol. 4424, pp. 87–101. Springer, Heidelberg (2007)

    Chapter  Google Scholar 

  18. Lang, F.: Refined interfaces for compositional verification. In: Najm, E., Pradat-Peyre, J.-F., Donzeau-Gouge, V.V. (eds.) FORTE 2006. LNCS, vol. 4229, pp. 159–174. Springer, Heidelberg (2006)

    Chapter  Google Scholar 

  19. Lynch, N., Tuttle, M.: An introduction to input/output automata. CWI Quarterly 2(3), 219–246 (1989)

    MATH  MathSciNet  Google Scholar 

  20. Mateescu, R.: Local model-checking of modal mu-calculus on acyclic labeled transition systems. In: Katoen, J.-P., Stevens, P. (eds.) TACAS 2002. LNCS, vol. 2280, pp. 281–295. Springer, Heidelberg (2002)

    Chapter  Google Scholar 

  21. Milner, R.: Communication and Concurrency. Prentice Hall, Englewood Cliffs (1989)

    MATH  Google Scholar 

  22. Paige, R., Tarjan, R.E.: Three partition refinement algorithms. SIAM J. Comput. 16(6), 973–989 (1987)

    Article  MATH  MathSciNet  Google Scholar 

  23. Simon, K.: An improved algorithm for transitive closure on acyclic digraphs. In: Kott, L. (ed.) ICALP 1986. LNCS, vol. 226, pp. 376–386. Springer, Heidelberg (1986)

    Google Scholar 

  24. Vesely, W., Goldberg, F., Roberts, N., Haasl, D.: Fault Tree Handbook. NASA (1981)

    Google Scholar 

  25. Wimmer, R., Herbstritt, M., Hermanns, H., Strampp, K., Becker, B.: Sigref- a symbolic bisimulation tool box. In: ATVA, pp. 477–492 (2006)

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Universität des Saarlandes, Saarbrücken, Germany

    Pepijn Crouzen, Holger Hermanns & Lijun Zhang

  2. INRIA, VASY, Grenoble Rhône-Alpes, France

    Holger Hermanns

Authors
  1. Pepijn Crouzen
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Holger Hermanns
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. Lijun Zhang
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Franck van Breugel Marsha Chechik

Rights and permissions

Reprints and permissions

Copyright information

© 2008 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Crouzen, P., Hermanns, H., Zhang, L. (2008). On the Minimisation of Acyclic Models. In: van Breugel, F., Chechik, M. (eds) CONCUR 2008 - Concurrency Theory. CONCUR 2008. Lecture Notes in Computer Science, vol 5201. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-85361-9_25

Download citation

  • DOI: https://doi.org/10.1007/978-3-540-85361-9_25

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-85360-2

  • Online ISBN: 978-3-540-85361-9

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics