Compositional Reasoning for Parametric Probabilistic Automata
Mertens, Hannah, Quatmann, Tim, Katoen, Joost-Pieter · DROPS (Schloss Dagstuhl – Leibniz Center for Informatics) · 2025
We establish an assume-guarantee (AG) framework for compositional reasoning about multi-objective queries in parametric probabilistic automata (pPA) - an extension to probabilistic automata (PA), where transition probabilities are functions over a finite set of parameters. We lift an existing framework for PA to the pPA setting, incorporating asymmetric, circular, and interleaving proof rules. Our approach enables the verification of a broad spectrum of multi-objective queries for pPA, encompassing probabilistic properties and (parametric) expected total rewards. Additionally, we introduce a rule for reasoning about monotonicity in composed pPAs.