Compositional Reasoning for Probabilistic Automata with Uncertainty

TL;DR

This paper introduces an assume-guarantee framework for compositional verification of probabilistic automata with uncertain transition probabilities, including parametric and robust variants, enabling multi-objective analysis.

Contribution

It extends existing AG frameworks to parametric and uncertain probabilistic automata, establishing new proof rules and simulation relations for compositional reasoning.

Findings

Established sound AG proof rules for convex rPAs and iPAs.

Developed a simulation-based AG style with strong simulation relations.

Identified limitations of AG reasoning for non-convex rPAs and memoryless semantics.

Abstract

This paper develops an assume-guarantee (AG) framework for the compositional verification of probabilistic automata (PAs) with uncertain transition probabilities. We study parametric probabilistic automata (pPAs), where probabilities are given by polynomial functions over a finite set of real-valued parameters and robust probabilistic automata (rPAs)-a generalisation of interval probabilistic automata (iPAs)-where transition probabilities range over potentially uncountable uncertainty sets. Towards pPAs, an existing AG framework for PAs is lifted to the parametric setting. We establish asymmetric, circular, and interleaving proof rules to enable compositional verification of a broad class of multi-objective queries, encompassing probabilistic reachability properties and parametric expected total rewards. In addition, we introduce a dedicated AG rule for compositional reasoning about parameter monotonicity. For convex rPAs and iPAs with history-dependent (memory-full) nature, we establish sound AG rules via a reduction to infinite PAs. We further show that AG reasoning can not straightforwardly be applied to non-convex rPAs, memoryless (once-and-for-all) nature semantics, and the common interval-arithmetic relaxation of parallel composition. Finally, we develop a simulation-based AG style for pPAs: we define strong simulation and robust-strong simulation relations for pPAs and derive their corresponding proof rules.