Logical Characterization of Trace Metrics

Valentina Castiglioni
(University of Insubria)
Simone Tini
(University of Insubria)

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 Herbert Wiklicky and Erik de Vink: Proceedings 15th Workshop on Quantitative Aspects of Programming Languages and Systems (QAPL 2017), Uppsala, Sweden, 23rd April 2017, Electronic Proceedings in Theoretical Computer Science 250, pp. 39–74.
Published: 12th July 2017.

ArXived at: http://dx.doi.org/10.4204/EPTCS.250.4 bibtex PDF
References in reconstructed bibtex, XML and HTML format (approximated).
Comments and questions to: eptcs@eptcs.org
For website issues: webmaster@eptcs.org