2014 14th International Conference on Application of Concurrency to System Design (2014)
Tunis La Marsa, Tunisia
June 23, 2014 to June 27, 2014
DOI Bookmark: http://doi.ieeecomputersociety.org/10.1109/ACSD.2014.10
Abstract probabilistic automata (APAs) constitute a complete abstraction and specification theory for probabilistic automata (PAs) [7, 8]. APA specifications support compositionality together with a step-wise refinement methodology, and thus are useful for component-oriented design and analysis of randomized distributed systems. This paper proposes a state-space reduction technique for such systems that are modeled as a network of acyclic APAs. Our technique is based on the notion of layered transformation. We propose a layered composition operator for acyclic APAs, and prove the communication closed layer (CCL) laws. Next, we define a partial order (po) equivalence between acyclic APAs, and show that it enables performing layered transformation within the framework of CCL laws. We also show the preservation of extremal reachability probabilities under this transformation.
Abstracts, Probabilistic logic, Automata, Distributed algorithms, Protocols, Real-time systems, Synchronization
A. Sharma and J. Katoen, "Layered Reduction for Abstract Probabilistic Automata," 2014 14th International Conference on Application of Concurrency to System Design(ACSD), Tunis La Marsa, Tunisia, 2014, pp. 21-31.