Logical Characterization of Bisimulation Metrics

Bisimulation metrics provide a robust and accurate approach to study the behavior of nondeterministic probabilistic processes. In this paper, we propose a logical characterization of bisimulation metrics based on a simple probabilistic variant of the Hennessy-Milner logic. Our approach is based on t...

Full description

Bibliographic Details
Main Authors: Valentina Castiglioni, Daniel Gebler, Simone Tini
Format: Article
Language:English
Published: Open Publishing Association 2016-10-01
Series:Electronic Proceedings in Theoretical Computer Science
Online Access:http://arxiv.org/pdf/1610.08169v1
_version_ 1818331881298460672
author Valentina Castiglioni
Daniel Gebler
Simone Tini
author_facet Valentina Castiglioni
Daniel Gebler
Simone Tini
author_sort Valentina Castiglioni
collection DOAJ
description Bisimulation metrics provide a robust and accurate approach to study the behavior of nondeterministic probabilistic processes. In this paper, we propose a logical characterization of bisimulation metrics based on a simple probabilistic variant of the Hennessy-Milner logic. Our approach is based on the novel notions of mimicking formulae and distance between formulae. The former are a weak version of the well known characteristic formulae and allow us to characterize also (ready) probabilistic simulation and probabilistic bisimilarity. The latter is a 1-bounded pseudometric on formulae that mirrors the Hausdorff and Kantorovich lifting the defining bisimilarity pseudometric. We show that the distance between two processes equals the distance between their own mimicking formulae.
first_indexed 2024-12-13T13:26:53Z
format Article
id doaj.art-d21b5dfdea9740a88b354c995859a7c7
institution Directory Open Access Journal
issn 2075-2180
language English
last_indexed 2024-12-13T13:26:53Z
publishDate 2016-10-01
publisher Open Publishing Association
record_format Article
series Electronic Proceedings in Theoretical Computer Science
spelling doaj.art-d21b5dfdea9740a88b354c995859a7c72022-12-21T23:44:16ZengOpen Publishing AssociationElectronic Proceedings in Theoretical Computer Science2075-21802016-10-01227Proc. QAPL 2016446210.4204/EPTCS.227.4:4Logical Characterization of Bisimulation MetricsValentina Castiglioni0Daniel Gebler1Simone Tini2 University of Insubria VU University Amsterdam University of Insubria Bisimulation metrics provide a robust and accurate approach to study the behavior of nondeterministic probabilistic processes. In this paper, we propose a logical characterization of bisimulation metrics based on a simple probabilistic variant of the Hennessy-Milner logic. Our approach is based on the novel notions of mimicking formulae and distance between formulae. The former are a weak version of the well known characteristic formulae and allow us to characterize also (ready) probabilistic simulation and probabilistic bisimilarity. The latter is a 1-bounded pseudometric on formulae that mirrors the Hausdorff and Kantorovich lifting the defining bisimilarity pseudometric. We show that the distance between two processes equals the distance between their own mimicking formulae.http://arxiv.org/pdf/1610.08169v1
spellingShingle Valentina Castiglioni
Daniel Gebler
Simone Tini
Logical Characterization of Bisimulation Metrics
Electronic Proceedings in Theoretical Computer Science
title Logical Characterization of Bisimulation Metrics
title_full Logical Characterization of Bisimulation Metrics
title_fullStr Logical Characterization of Bisimulation Metrics
title_full_unstemmed Logical Characterization of Bisimulation Metrics
title_short Logical Characterization of Bisimulation Metrics
title_sort logical characterization of bisimulation metrics
url http://arxiv.org/pdf/1610.08169v1
work_keys_str_mv AT valentinacastiglioni logicalcharacterizationofbisimulationmetrics
AT danielgebler logicalcharacterizationofbisimulationmetrics
AT simonetini logicalcharacterizationofbisimulationmetrics