[EisentrautHSTZ13] The Quest for Minimal Quotients for Probabilistic Automata Eisentraut, C.; Hermanns, H.; Schuster, J.; Turrini, A. and Zhang, L. In Tools and Algorithms for the Construction and Analysis of Systems - 19th International Conference (TACAS), pages 16-31, Springer, Lecture Notes in Computer Science 7795, 2013.
Downloads: pdf, bibURL: http://dx.doi.org/10.1007/978-3-642-36742-7_2 Abstract. One of the prevailing ideas in applied concurrency theory and verification is the concept of automata minimization with respect to strong or weak bisimilarity. The minimal automata can be seen as canonical representations of the behaviour modulo the bisimilarity considered. Together with congruence results wrt. process algebraic operators, this can be exploited to alleviate the notorious state space explosion problem. In this paper, we aim at identifying minimal automata and canonical representations for concurrent probabilistic models. We present minimality and canonicity results for probabilistic automata wrt. strong and weak bisimilarity, together with polynomial time minimization algorithms.