The Quest for Minimal Quotients for Probabilistic Automata
|Title||The Quest for Minimal Quotients for Probabilistic Automata|
|Publication Type||Conference Paper|
|Year of Publication||2013|
|Authors||Eisentraut C.W, Hermanns H., Schuster J., Turini A., Zhang L.|
|Conference Name||19th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS), Rome, Italy|
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.