Logical Characterization of Trace Metrics

TL;DR

This paper develops a logical framework to characterize strong and weak trace metrics in nondeterministic probabilistic processes, linking logical properties with behavioral metrics and model checking.

Contribution

It introduces a minimal boolean logic capable of characterizing probabilistic trace equivalences and connects this approach to classical probabilistic model checking.

Findings

Logical characterization of strong and weak trace metrics

Minimal boolean logic suffices for probabilistic trace equivalence

Connection established between logical characterization and model checking

Abstract

In this paper we continue our research line on logical characterizations of behavioral metrics obtained from the definition of a metric over the set of logical properties of interest. This time we provide a characterization of both strong and weak trace metric on nondeterministic probabilistic processes, based on a minimal boolean logic L which we prove to be powerful enough to characterize strong and weak probabilistic trace equivalence. Moreover, we also prove that our characterization approach can be restated in terms of a more classic probabilistic L-model checking problem.