×

On the minimisation of acyclic models. (English) Zbl 1160.68462

van Breugel, Franck (ed.) et al., CONCUR 2008 – concurrency theory. 19th international conference, CONCUR 2008, Toronto, Canada, August 19–22, 2008. Proceedings. Berlin: Springer (ISBN 978-3-540-85360-2/pbk). Lecture Notes in Computer Science 5201, 295-309 (2008).
Summary: 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.
For the entire collection see [Zbl 1149.68018].

MSC:

68Q85 Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.)
PDFBibTeX XMLCite
Full Text: DOI

References:

[1] Blom, S.; Fokkink, W.; Groote, J. F.; van Langevelde, I.; Lisser, B.; van de Pol, J.; Berry, G.; Comon, H.; Finkel, A., μcrl: A toolset for analysing algebraic specifications, Computer Aided Verification, 250-254 (2001), Heidelberg: Springer, Heidelberg · Zbl 0991.68640
[2] Blom, S., Orzan, S.: Distributed branching bisimulation reduction of state spaces. Electr. Notes Theor. Comput. Sci. 89(1) (2003) · Zbl 1271.68133
[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)
[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) · Zbl 1141.68454
[5] Bravetti, M.: Revisiting interactive markov chains. Electronic Notes in Theoretical Computer Science 68(5) (2002) · Zbl 1270.68207
[6] Coppersmith, D., Winograd, S.: Matrix multiplication via arithmetic progressions. In: ACM Symposium on Theory of Computing (1987) · Zbl 0702.65046
[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)
[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.; Berry, G.; Comon, H.; Finkel, A., A fast bisimulation algorithm, Computer Aided Verification, 79-90 (2001), Heidelberg: Springer, Heidelberg · Zbl 0991.68553
[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) · Zbl 0825.68162
[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) · Zbl 1103.68652
[12] Garavel, H., Lang, F., Mateescu, R., Serwe, W.: Cadp 2006: A toolbox for the construction and analysis of distributed processes. In: CAV (2006) · Zbl 1316.68074
[13] Goralcikova, A.; Koubek, V., A reduct-and-closure algorithm for graphs, Mathematical Foundations of Computer Science, 74, 301-307 (1979) · Zbl 0408.68038
[14] Griffioen, W. O.D.; Vaandrager, F. W., A theory of normed simulations, ACM Trans. Comput. Log., 5, 4, 577-610 (2004) · Zbl 1367.68192
[15] Groote, J. F.; Vaandrager, F.; Paterson, M., An efficient algorithm for branching bisimulation and stuttering equivalence, Automata, Languages and Programming (1990), Heidelberg: Springer, Heidelberg · Zbl 0765.68125
[16] Hermanns, H., Interactive Markov Chains: The Quest for Quantified Quality (2002), Heidelberg: Springer, Heidelberg · Zbl 1012.68142
[17] Katoen, J.-P.; Kemna, T.; Zapreev, I. S.; Jansen, D. N.; Grumberg, O.; Huth, M., Bisimulation minimisation mostly speeds up probabilistic model checking, Tools and Algorithms for the Construction and Analysis of Systems, 87-101 (2007), Heidelberg: Springer, Heidelberg · Zbl 1186.68296
[18] Lang, F.; Najm, E.; Pradat-Peyre, J.-F.; Donzeau-Gouge, V. V., Refined interfaces for compositional verification, Formal Techniques for Networked and Distributed Systems - FORTE 2006, 159-174 (2006), Heidelberg: Springer, Heidelberg · Zbl 1225.68120
[19] Lynch, N.; Tuttle, M., An introduction to input/output automata, CWI Quarterly, 2, 3, 219-246 (1989) · Zbl 0677.68067
[20] Mateescu, R.; Katoen, J.-P.; Stevens, P., Local model-checking of modal mu-calculus on acyclic labeled transition systems, Tools and Algorithms for the Construction and Analysis of Systems, 281-295 (2002), Heidelberg: Springer, Heidelberg · Zbl 1043.68596
[21] Milner, R., Communication and Concurrency (1989), Englewood Cliffs: Prentice Hall, Englewood Cliffs · Zbl 0683.68008
[22] Paige, R.; Tarjan, R. E., Three partition refinement algorithms, SIAM J. Comput., 16, 6, 973-989 (1987) · Zbl 0654.68072
[23] Simon, K.; Kott, L., An improved algorithm for transitive closure on acyclic digraphs, Automata, Languages and Programming, 376-386 (1986), Heidelberg: Springer, Heidelberg · Zbl 0595.68044
[24] Vesely, W., Goldberg, F., Roberts, N., Haasl, D.: Fault Tree Handbook. NASA (1981)
[25] Wimmer, R., Herbstritt, M., Hermanns, H., Strampp, K., Becker, B.: Sigref- a symbolic bisimulation tool box. In: ATVA, pp. 477-492 (2006) · Zbl 1161.68631
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.