Publication

[CrouzenHZ08] On the Minimisation of Acyclic Models Crouzen, P.; Hermanns, H. and Zhang, L. In Concurrency Theory, 19th International Conference (CONCUR), pages 295-309, Springer, Lecture Notes in Computer Science 5201, 2008.
Downloads: pdf, bibURL: http://dx.doi.org/10.1007/978-3-540-85361-9_25 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.