The Quest for Minimal Quotients for Probabilistic Automata

TitleThe Quest for Minimal Quotients for Probabilistic Automata
Publication TypeConference Paper
Year of Publication2013
AuthorsEisentraut C.W, Hermanns H., Schuster J., Turini A., Zhang L.
Conference Name19th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS), Rome, Italy
Date PublishedMarch
Conference LocationBerlin

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.