Linear and Branching System Metrics

Hilston J. (Editor), Luca de Alfaro, Marco Faella, Kwiatkowska M.Z. (Editor), M. Telek (Editor), Mariëlle Ida Antoinette Stoelinga

Research output: Contribution to journalArticleAcademicpeer-review

58 Citations (Scopus)
16 Downloads (Pure)

Abstract

We extend the classical 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 elements of arbitrary metric spaces. 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 metric transition systems. Finally, we provide algorithms for computing the distances over finite systems, together with a matching lower complexity bound.
Original languageUndefined
Article number10.1109/TSE.2008.106
Pages (from-to)258-273
Number of pages16
JournalIEEE transactions on software engineering
Volume35
Issue number2
DOIs
Publication statusPublished - Mar 2009

Keywords

  • IR-68677
  • METIS-264177
  • EWI-16577
  • EC Grant Agreement nr.: IST-004527
  • EC Grant Agreement nr.: FP7/214755
  • EC Grant Agreement nr.: FP7-ICT-2007-1
  • Specification techniques
  • Modal logic
  • Logics of programs

Cite this

J., H. (Ed.), de Alfaro, L., Faella, M., M.Z., K. (Ed.), Telek, M. (Ed.), & Stoelinga, M. I. A. (2009). Linear and Branching System Metrics. IEEE transactions on software engineering, 35(2), 258-273. [10.1109/TSE.2008.106]. https://doi.org/10.1109/TSE.2008.106
J., Hilston (Editor) ; de Alfaro, Luca ; Faella, Marco ; M.Z., Kwiatkowska (Editor) ; Telek, M. (Editor) ; Stoelinga, Mariëlle Ida Antoinette. / Linear and Branching System Metrics. In: IEEE transactions on software engineering. 2009 ; Vol. 35, No. 2. pp. 258-273.
@article{6917994091bd4bacab31032c6e595df9,
title = "Linear and Branching System Metrics",
abstract = "We extend the classical 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 elements of arbitrary metric spaces. 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 metric transition systems. Finally, we provide algorithms for computing the distances over finite systems, together with a matching lower complexity bound.",
keywords = "IR-68677, METIS-264177, EWI-16577, EC Grant Agreement nr.: IST-004527, EC Grant Agreement nr.: FP7/214755, EC Grant Agreement nr.: FP7-ICT-2007-1, Specification techniques, Modal logic, Logics of programs",
author = "Hilston J. and {de Alfaro}, Luca and Marco Faella and Kwiatkowska M.Z. and M. Telek and Stoelinga, {Mari{\"e}lle Ida Antoinette}",
note = "eemcs-eprint-16577",
year = "2009",
month = "3",
doi = "10.1109/TSE.2008.106",
language = "Undefined",
volume = "35",
pages = "258--273",
journal = "IEEE transactions on software engineering",
issn = "0098-5589",
publisher = "IEEE",
number = "2",

}

J., H (ed.), de Alfaro, L, Faella, M, M.Z., K (ed.), Telek, M (ed.) & Stoelinga, MIA 2009, 'Linear and Branching System Metrics' IEEE transactions on software engineering, vol. 35, no. 2, 10.1109/TSE.2008.106, pp. 258-273. https://doi.org/10.1109/TSE.2008.106

Linear and Branching System Metrics. / J., Hilston (Editor); de Alfaro, Luca; Faella, Marco; M.Z., Kwiatkowska (Editor); Telek, M. (Editor); Stoelinga, Mariëlle Ida Antoinette.

In: IEEE transactions on software engineering, Vol. 35, No. 2, 10.1109/TSE.2008.106, 03.2009, p. 258-273.

Research output: Contribution to journalArticleAcademicpeer-review

TY - JOUR

T1 - Linear and Branching System Metrics

AU - de Alfaro, Luca

AU - Faella, Marco

AU - Stoelinga, Mariëlle Ida Antoinette

A2 - J., Hilston

A2 - M.Z., Kwiatkowska

A2 - Telek, M.

N1 - eemcs-eprint-16577

PY - 2009/3

Y1 - 2009/3

N2 - We extend the classical 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 elements of arbitrary metric spaces. 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 metric transition systems. Finally, we provide algorithms for computing the distances over finite systems, together with a matching lower complexity bound.

AB - We extend the classical 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 elements of arbitrary metric spaces. 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 metric transition systems. Finally, we provide algorithms for computing the distances over finite systems, together with a matching lower complexity bound.

KW - IR-68677

KW - METIS-264177

KW - EWI-16577

KW - EC Grant Agreement nr.: IST-004527

KW - EC Grant Agreement nr.: FP7/214755

KW - EC Grant Agreement nr.: FP7-ICT-2007-1

KW - Specification techniques

KW - Modal logic

KW - Logics of programs

U2 - 10.1109/TSE.2008.106

DO - 10.1109/TSE.2008.106

M3 - Article

VL - 35

SP - 258

EP - 273

JO - IEEE transactions on software engineering

JF - IEEE transactions on software engineering

SN - 0098-5589

IS - 2

M1 - 10.1109/TSE.2008.106

ER -

J. H, (ed.), de Alfaro L, Faella M, M.Z. K, (ed.), Telek M, (ed.), Stoelinga MIA. Linear and Branching System Metrics. IEEE transactions on software engineering. 2009 Mar;35(2):258-273. 10.1109/TSE.2008.106. https://doi.org/10.1109/TSE.2008.106