Layered Reduction for Abstract Probabilistic Automata

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.