Compositional Reasoning for Parametric Probabilistic Automata
Fuente:
arXiv
Guardado en:
| Autores principales: | , , |
|---|---|
| Formato: | Preprint |
| Publicado: |
2025
|
| Materias: | |
| Acceso en línea: | |
| Etiquetas: |
Agregar Etiqueta
Sin Etiquetas, Sea el primero en etiquetar este registro!
|
| _version_ | 1866913887659491328 |
|---|---|
| author | Mertens, Hannah Quatmann, Tim Katoen, Joost-Pieter |
| author_facet | Mertens, Hannah Quatmann, Tim Katoen, Joost-Pieter |
| contents | 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. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2506_08525 |
| institution | arXiv |
| publishDate | 2025 |
| record_format | arxiv |
| spellingShingle | Compositional Reasoning for Parametric Probabilistic Automata Mertens, Hannah Quatmann, Tim Katoen, Joost-Pieter Logic in Computer Science Probability 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. |
| title | Compositional Reasoning for Parametric Probabilistic Automata |
| topic | Logic in Computer Science Probability |
| url | https://arxiv.org/abs/2506.08525 |