Logical Characterization of Trace Metrics

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.

In Proceedings QAPL 2017, arXiv:1707.03668

References in corpus (4)

• Revisiting Trace and Testing Equivalences for Nondeterministic and Probabilistic Processes
• Logical, Metric, and Algorithmic Characterisations of Probabilistic Bisimulation
• Logical Characterization of Bisimulation Metrics
• Linear Distances between Markov Chains

Cited by in corpus (1)

• Quantitative Aspects of Programming Languages and Systems over the past $2^4$ years and beyond