Compositional Reasoning for Parametric Probabilistic Automata

TL;DR

This paper develops a compositional reasoning framework for parametric probabilistic automata, enabling multi-objective verification including probabilistic and reward properties, with new proof rules and monotonicity reasoning.

Contribution

It extends existing probabilistic automata frameworks to parametric settings, introducing novel proof rules and monotonicity reasoning for compositional verification.

Findings

Framework supports multi-objective queries in pPA

Incorporates new proof rules for complex compositions

Enables verification of probabilistic and reward properties

Abstract

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.