The Quest for Minimal Quotients for Probabilistic Automata

Christian Eisentraut, Holger Hermanns, Johann Schuster, Andrea Turrini, Lijun Zhang

Research output: Chapter in Book/Report/Conference proceedingArticle in proceedingsResearchpeer-review

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.
Original languageEnglish
Title of host publicationTools and Algorithms for the Construction and Analysis of Systems : 19th International Conference, TACAS 2013, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2013, Rome, Italy, March 16-24, 2013. Proceedings
PublisherSpringer
Publication date2013
Pages16-31
ISBN (Print)978-3-642-36741-0
ISBN (Electronic)978-3-642-36742-7
DOIs
Publication statusPublished - 2013
Event19th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS 2013) - Rome, Italy
Duration: 16 Mar 201324 Mar 2013
http://www.etaps.org/2013/tacas13

Conference

Conference19th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS 2013)
CountryItaly
CityRome
Period16/03/201324/03/2013
Internet address
SeriesLecture Notes in Computer Science
Volume7795
ISSN0302-9743

Keywords

  • Algorithms
  • Polynomial approximation
  • Automata theory

Fingerprint Dive into the research topics of 'The Quest for Minimal Quotients for Probabilistic Automata'. Together they form a unique fingerprint.

Cite this