2025/06/10 by Hannah Mertens, Mertens, Hannah, Tim Quatmann +3
Computer Science · #Formal Methods in Verification #Logic, Reasoning, and Knowledge #Bayesian Modeling and Causal Inference
paper · doi:10.48550/arxiv.2506.08525
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.