2012 | OriginalPaper | Buchkapitel
Compositional Abstraction Techniques for Probabilistic Automata
verfasst von : Falak Sher, Joost-Pieter Katoen
Erschienen in: Theoretical Computer Science
Verlag: Springer Berlin Heidelberg
Aktivieren Sie unsere intelligente Suche, um passende Fachinhalte oder Patente zu finden.
Wählen Sie Textabschnitte aus um mit Künstlicher Intelligenz passenden Patente zu finden. powered by
Markieren Sie Textabschnitte, um KI-gestützt weitere passende Inhalte zu finden. powered by
We present aggressive abstraction techniques for probabilistic automata (PA), a state-based model involving discrete probabilistic and nondeterministic branching. Our abstractions yield
abstract
PA in which transitions are typed “possible” or “required”—as in modal transition systems—and have constraint functions as target. The key idea is to focus on identifying common combined-transitions from concrete states and putting them as required ones in the abstract state. We prove the correctness of our abstraction techniques, study their relationship, and show that they are
compositional
w.r.t. parallel composition. We also show the preservation of probabilistic and expected reachability properties for PA.