On the Relationship between Bisimulation and Trace Equivalence in an Approximate Probabilistic Context (Extended Version)

TL;DR

This paper introduces a new notion of approximate probabilistic trace equivalence for labelled Markov chains, relating it to bisimulation, and demonstrates its applications in model checking and synthesizing approximations for continuous models.

Contribution

It establishes a tight upper bound on trace approximation via bisimulation, extending existing results to probabilistic and uncountable-state models.

Findings

Bisimulation induces a tight upper bound on trace distance.

The bound aids in probabilistic model checking of concrete models.

It enables synthesis of precise discrete approximations to continuous models.

Abstract

This work introduces a notion of approximate probabilistic trace equivalence for labelled Markov chains, and relates this new concept to the known notion of approximate probabilistic bisimulation. In particular this work shows that the latter notion induces a tight upper bound on the approximation between finite-horizon traces, as expressed by a total variation distance. As such, this work extends corresponding results for exact notions and analogous results for non-probabilistic models. This bound can be employed to relate the closeness in satisfaction probabilities over bounded linear-time properties, and allows for probabilistic model checking of concrete models via abstractions. The contribution focuses on both finite-state and uncountable-state labelled Markov chains, and claims two main applications: firstly, it allows an upper bound on the trace distance to be decided for finite state systems; secondly, it can be used to synthesise discrete approximations to continuous-state models with arbitrary precision.