Cost Preserving Bisimulations for Probabilistic Automata

TL;DR

This paper extends probabilistic automata with cost measures, introducing cost-preserving bisimulations and decision algorithms to analyze and abstract probabilistic systems efficiently.

Contribution

It develops cost-preserving and cost-bounding bisimulations for probabilistic automata, with compositional properties and polynomial-time algorithms for abstraction.

Findings

Introduces cost-aware weak probabilistic bisimulations.

Establishes compositionality of cost-preserving bisimulations.

Provides polynomial-time algorithms for reward-bounding abstractions.

Abstract

Probabilistic automata constitute a versatile and elegant model for concurrent probabilistic systems. They are equipped with a compositional theory supporting abstraction, enabled by weak probabilistic bisimulation serving as the reference notion for summarising the effect of abstraction. This paper considers probabilistic automata augmented with costs. It extends the notions of weak transitions in probabilistic automata in such a way that the costs incurred along a weak transition are captured. This gives rise to cost-preserving and cost-bounding variations of weak probabilistic bisimilarity, for which we establish compositionality properties with respect to parallel composition. Furthermore, polynomial-time decision algorithms are proposed, that can be effectively used to compute reward-bounding abstractions of Markov decision processes in a compositional manner.