Linear and Branching Metrics for Quantitative Transition Systems

Luca de Alfaro, Marco Faella, Mariëlle Ida Antoinette Stoelinga

Research output: Contribution to conferencePaperAcademicpeer-review

Abstract

We extend the basic system relations of trace inclusion, trace equivalence, simulation, and bisimulation to a quantitative setting in which propositions are interpreted not as boolean values, but as real values in the interval [0,1]. Trace inclusion and equivalence give rise to asymmetrical and symmetrical linear distances, while simulation and bisimulation give rise to asymmetrical and symmetrical branching distances. We study the relationships among these distances, and we provide a full logical characterization of the distances in terms of quantitative versions of Ltl and -calculus. We show that, while trace inclusion (resp. equivalence) coincides with simulation (resp. bisimulation) for deterministic boolean transition systems, linear and branching distances do not coincide for deterministic quantitative transition systems. Finally, we provide algorithms for computing the distances, together with matching lower and upper complexity bounds. This research was supported in part by the NSF CAREER grant CCR-0132780, the NSF grant CCR-0234690, and the ONR grant N00014-02-1-0671.
Original languageUndefined
Pages97-109
Number of pages13
DOIs
Publication statusPublished - 2004

Keywords

  • IR-63332
  • EWI-6550

Cite this

@conference{6529413a9a354a5fa4d4f14a8c812d6f,
title = "Linear and Branching Metrics for Quantitative Transition Systems",
abstract = "We extend the basic system relations of trace inclusion, trace equivalence, simulation, and bisimulation to a quantitative setting in which propositions are interpreted not as boolean values, but as real values in the interval [0,1]. Trace inclusion and equivalence give rise to asymmetrical and symmetrical linear distances, while simulation and bisimulation give rise to asymmetrical and symmetrical branching distances. We study the relationships among these distances, and we provide a full logical characterization of the distances in terms of quantitative versions of Ltl and -calculus. We show that, while trace inclusion (resp. equivalence) coincides with simulation (resp. bisimulation) for deterministic boolean transition systems, linear and branching distances do not coincide for deterministic quantitative transition systems. Finally, we provide algorithms for computing the distances, together with matching lower and upper complexity bounds. This research was supported in part by the NSF CAREER grant CCR-0132780, the NSF grant CCR-0234690, and the ONR grant N00014-02-1-0671.",
keywords = "IR-63332, EWI-6550",
author = "{de Alfaro}, Luca and Marco Faella and Stoelinga, {Mari{\"e}lle Ida Antoinette}",
year = "2004",
doi = "10.1007/b99859",
language = "Undefined",
pages = "97--109",

}

Linear and Branching Metrics for Quantitative Transition Systems. / de Alfaro, Luca; Faella, Marco; Stoelinga, Mariëlle Ida Antoinette.

2004. 97-109.

Research output: Contribution to conferencePaperAcademicpeer-review

TY - CONF

T1 - Linear and Branching Metrics for Quantitative Transition Systems

AU - de Alfaro, Luca

AU - Faella, Marco

AU - Stoelinga, Mariëlle Ida Antoinette

PY - 2004

Y1 - 2004

N2 - We extend the basic system relations of trace inclusion, trace equivalence, simulation, and bisimulation to a quantitative setting in which propositions are interpreted not as boolean values, but as real values in the interval [0,1]. Trace inclusion and equivalence give rise to asymmetrical and symmetrical linear distances, while simulation and bisimulation give rise to asymmetrical and symmetrical branching distances. We study the relationships among these distances, and we provide a full logical characterization of the distances in terms of quantitative versions of Ltl and -calculus. We show that, while trace inclusion (resp. equivalence) coincides with simulation (resp. bisimulation) for deterministic boolean transition systems, linear and branching distances do not coincide for deterministic quantitative transition systems. Finally, we provide algorithms for computing the distances, together with matching lower and upper complexity bounds. This research was supported in part by the NSF CAREER grant CCR-0132780, the NSF grant CCR-0234690, and the ONR grant N00014-02-1-0671.

AB - We extend the basic system relations of trace inclusion, trace equivalence, simulation, and bisimulation to a quantitative setting in which propositions are interpreted not as boolean values, but as real values in the interval [0,1]. Trace inclusion and equivalence give rise to asymmetrical and symmetrical linear distances, while simulation and bisimulation give rise to asymmetrical and symmetrical branching distances. We study the relationships among these distances, and we provide a full logical characterization of the distances in terms of quantitative versions of Ltl and -calculus. We show that, while trace inclusion (resp. equivalence) coincides with simulation (resp. bisimulation) for deterministic boolean transition systems, linear and branching distances do not coincide for deterministic quantitative transition systems. Finally, we provide algorithms for computing the distances, together with matching lower and upper complexity bounds. This research was supported in part by the NSF CAREER grant CCR-0132780, the NSF grant CCR-0234690, and the ONR grant N00014-02-1-0671.

KW - IR-63332

KW - EWI-6550

U2 - 10.1007/b99859

DO - 10.1007/b99859

M3 - Paper

SP - 97

EP - 109

ER -