Skip to Main content Skip to Navigation
Conference papers

Compositional Abstraction Techniques for Probabilistic Automata

Abstract : 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.
Document type :
Conference papers
Complete list of metadata

Cited literature [15 references]  Display  Hide  Download

https://hal.inria.fr/hal-01556222
Contributor : Hal Ifip <>
Submitted on : Tuesday, July 4, 2017 - 5:45:44 PM
Last modification on : Monday, July 8, 2019 - 3:30:02 PM
Long-term archiving on: : Friday, December 15, 2017 - 1:48:59 AM

File

978-3-642-33475-7_23_Chapter.p...
Files produced by the author(s)

Licence


Distributed under a Creative Commons Attribution 4.0 International License

Identifiers

Citation

Falak Sher, Joost-Pieter Katoen. Compositional Abstraction Techniques for Probabilistic Automata. 7th International Conference on Theoretical Computer Science (TCS), Sep 2012, Amsterdam, Netherlands. pp.325-341, ⟨10.1007/978-3-642-33475-7_23⟩. ⟨hal-01556222⟩

Share

Metrics

Record views

96

Files downloads

175