Linear and branching metrics for quantitative transition systems

L. de Alfaro; M. Faella; Mariëlle Ida Antoinette Stoelinga

doi:10.1007/978-3-540-27836-8_11

Linear and branching metrics for quantitative transition systems

L. de Alfaro, M. Faella, Mariëlle Ida Antoinette Stoelinga

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution › Academic › peer-review

67 Citations (Scopus)

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.

Original language	English
Title of host publication	Automata, Languages and Programming
Subtitle of host publication	31st International Colloquium, ICALP 2004, Turku, Finland, July 12-16, 2004. Proceedings
Editors	J. Díaz, J. Karhumäki, A. Lepistö, D. Sannella
Place of Publication	Berlin
Publisher	Springer
Pages	97-109
ISBN (Electronic)	978-3-540-27836-8
ISBN (Print)	978-3-540-22849-3
DOIs	https://doi.org/10.1007/978-3-540-27836-8_11
Publication status	Published - 12 Jul 2004
Event	31st International Colloquium on Automata, Languages and Programming, ICALP 2004 - Turku University, Turku, Finland Duration: 12 Jul 2004 → 16 Jul 2004 Conference number: 31 http://www.math.utu.fi/projects/icalp2004/

Publication series

Name	Lecture Notes in Computer Science
Publisher	Springer
Volume	3142
ISSN (Print)	0302-9743
ISSN (Electronic)	1611-3349

Workshop

Workshop	31st International Colloquium on Automata, Languages and Programming, ICALP 2004
Abbreviated title	ICALP
Country/Territory	Finland
City	Turku
Period	12/07/04 → 16/07/04
Internet address	http://www.math.utu.fi/projects/icalp2004/

Keywords

METIS-221392

Access to Document

10.1007/978-3-540-27836-8_11

Cite this

de Alfaro, L., Faella, M., & Stoelinga, M. I. A. (2004). Linear and branching metrics for quantitative transition systems. In J. Díaz, J. Karhumäki, A. Lepistö, & D. Sannella (Eds.), Automata, Languages and Programming: 31st International Colloquium, ICALP 2004, Turku, Finland, July 12-16, 2004. Proceedings (pp. 97-109). (Lecture Notes in Computer Science; Vol. 3142). Springer. https://doi.org/10.1007/978-3-540-27836-8_11

de Alfaro, L. ; Faella, M. ; Stoelinga, Mariëlle Ida Antoinette. / Linear and branching metrics for quantitative transition systems. Automata, Languages and Programming: 31st International Colloquium, ICALP 2004, Turku, Finland, July 12-16, 2004. Proceedings. editor / J. Díaz ; J. Karhumäki ; A. Lepistö ; D. Sannella. Berlin : Springer, 2004. pp. 97-109 (Lecture Notes in Computer Science).

@inproceedings{bb55def7ca8c42418d0a631d83880367,

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.",

keywords = "METIS-221392",

author = "{de Alfaro}, L. and M. Faella and Stoelinga, {Mari{\"e}lle Ida Antoinette}",

year = "2004",

month = jul,

day = "12",

doi = "10.1007/978-3-540-27836-8_11",

language = "English",

isbn = "978-3-540-22849-3",

series = "Lecture Notes in Computer Science",

publisher = "Springer",

pages = "97--109",

editor = "J. D{\'i}az and J. Karhum{\"a}ki and A. Lepist{\"o} and D. Sannella",

booktitle = "Automata, Languages and Programming",

note = "31st International Colloquium on Automata, Languages and Programming, ICALP 2004, ICALP ; Conference date: 12-07-2004 Through 16-07-2004",

url = "http://www.math.utu.fi/projects/icalp2004/",

}

de Alfaro, L, Faella, M & Stoelinga, MIA 2004, Linear and branching metrics for quantitative transition systems. in J Díaz, J Karhumäki, A Lepistö & D Sannella (eds), Automata, Languages and Programming: 31st International Colloquium, ICALP 2004, Turku, Finland, July 12-16, 2004. Proceedings. Lecture Notes in Computer Science, vol. 3142, Springer, Berlin, pp. 97-109, 31st International Colloquium on Automata, Languages and Programming, ICALP 2004, Turku, Finland, 12/07/04. https://doi.org/10.1007/978-3-540-27836-8_11

Linear and branching metrics for quantitative transition systems. / de Alfaro, L.; Faella, M.; Stoelinga, Mariëlle Ida Antoinette.
Automata, Languages and Programming: 31st International Colloquium, ICALP 2004, Turku, Finland, July 12-16, 2004. Proceedings. ed. / J. Díaz; J. Karhumäki; A. Lepistö; D. Sannella. Berlin: Springer, 2004. p. 97-109 (Lecture Notes in Computer Science; Vol. 3142).

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution › Academic › peer-review

TY - GEN

T1 - Linear and branching metrics for quantitative transition systems

AU - de Alfaro, L.

AU - Faella, M.

AU - Stoelinga, Mariëlle Ida Antoinette

N1 - Conference code: 31

PY - 2004/7/12

Y1 - 2004/7/12

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.

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.

KW - METIS-221392

U2 - 10.1007/978-3-540-27836-8_11

DO - 10.1007/978-3-540-27836-8_11

M3 - Conference contribution

SN - 978-3-540-22849-3

T3 - Lecture Notes in Computer Science

SP - 97

EP - 109

BT - Automata, Languages and Programming

A2 - Díaz, J.

A2 - Karhumäki, J.

A2 - Lepistö, A.

A2 - Sannella, D.

PB - Springer

CY - Berlin

T2 - 31st International Colloquium on Automata, Languages and Programming, ICALP 2004

Y2 - 12 July 2004 through 16 July 2004

ER -

de Alfaro L, Faella M, Stoelinga MIA. Linear and branching metrics for quantitative transition systems. In Díaz J, Karhumäki J, Lepistö A, Sannella D, editors, Automata, Languages and Programming: 31st International Colloquium, ICALP 2004, Turku, Finland, July 12-16, 2004. Proceedings. Berlin: Springer. 2004. p. 97-109. (Lecture Notes in Computer Science). doi: 10.1007/978-3-540-27836-8_11

Linear and branching metrics for quantitative transition systems

Abstract

Publication series

Workshop

Keywords

Access to Document

Fingerprint

Cite this