Logical Characterization of Trace Metrics

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 proce...

Full description

Bibliographic Details
Main Authors: Valentina Castiglioni, Simone Tini
Format: Article
Language:English
Published: Open Publishing Association 2017-07-01
Series:Electronic Proceedings in Theoretical Computer Science
Online Access:http://arxiv.org/pdf/1707.04124v1
id doaj-8f86ea01b1624f3882e28599f349a7e6
record_format Article
spelling doaj-8f86ea01b1624f3882e28599f349a7e62020-11-25T01:15:32ZengOpen Publishing AssociationElectronic Proceedings in Theoretical Computer Science2075-21802017-07-01250Proc. QAPL 2017397410.4204/EPTCS.250.4:4Logical Characterization of Trace MetricsValentina Castiglioni0Simone Tini1 University of Insubria 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.http://arxiv.org/pdf/1707.04124v1
collection DOAJ
language English
format Article
sources DOAJ
author Valentina Castiglioni
Simone Tini
spellingShingle Valentina Castiglioni
Simone Tini
Logical Characterization of Trace Metrics
Electronic Proceedings in Theoretical Computer Science
author_facet Valentina Castiglioni
Simone Tini
author_sort Valentina Castiglioni
title Logical Characterization of Trace Metrics
title_short Logical Characterization of Trace Metrics
title_full Logical Characterization of Trace Metrics
title_fullStr Logical Characterization of Trace Metrics
title_full_unstemmed Logical Characterization of Trace Metrics
title_sort logical characterization of trace metrics
publisher Open Publishing Association
series Electronic Proceedings in Theoretical Computer Science
issn 2075-2180
publishDate 2017-07-01
description 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.
url http://arxiv.org/pdf/1707.04124v1
work_keys_str_mv AT valentinacastiglioni logicalcharacterizationoftracemetrics
AT simonetini logicalcharacterizationoftracemetrics
_version_ 1725152696512544768