Computing branching distances with quantitative games

Uli Fahrenberg; Axel Legay; Karin Quaas

doi:10.1016/j.tcs.2020.10.001

Computing branching distances with quantitative games

Uli Fahrenberg^*, Axel Legay, Karin Quaas

^*Corresponding author for this work

Research output: Contribution to journal › Journal article › Research › peer-review

2 Citations (Scopus)

Abstract

We lay out a general method for computing branching distances between labeled transition systems. We translate the quantitative games used for defining these distances to other, path-building games which are amenable to methods from the theory of quantitative games. We then show for all common types of branching distances how the resulting path-building games can be solved. In the end, we achieve a method which can be used to compute all branching distances in the linear-time–branching-time spectrum.

Original language	English
Journal	Theoretical Computer Science
Volume	847
Pages (from-to)	134-146
Number of pages	13
ISSN	0304-3975
DOIs	https://doi.org/10.1016/j.tcs.2020.10.001
Publication status	Published - 22 Dec 2020

Bibliographical note

Funding Information:
This author's work is supported by the Chaire ISC : Engineering Complex Systems – École Polytechnique Foundation – Thales – FX – DGA – Dassault Aviation – Naval Group – ENSTA Paris – Télécom Paris.

Publisher Copyright:
© 2020 Elsevier B.V.

Keywords

Branching distance
Path-building game
Quantitative game
Quantitative verification

Access to Document

10.1016/j.tcs.2020.10.001

AUB Link

Search for the material in Aalborg University Library's search engine

Cite this

@article{6a436712c3fc422f9fbadc4bb7fd4c93,

title = "Computing branching distances with quantitative games",

abstract = "We lay out a general method for computing branching distances between labeled transition systems. We translate the quantitative games used for defining these distances to other, path-building games which are amenable to methods from the theory of quantitative games. We then show for all common types of branching distances how the resulting path-building games can be solved. In the end, we achieve a method which can be used to compute all branching distances in the linear-time–branching-time spectrum.",

keywords = "Branching distance, Path-building game, Quantitative game, Quantitative verification",

author = "Uli Fahrenberg and Axel Legay and Karin Quaas",

note = "Funding Information: This author's work is supported by the Chaire ISC : Engineering Complex Systems – {\'E}cole Polytechnique Foundation – Thales – FX – DGA – Dassault Aviation – Naval Group – ENSTA Paris – T{\'e}l{\'e}com Paris. Publisher Copyright: {\textcopyright} 2020 Elsevier B.V.",

year = "2020",

month = dec,

day = "22",

doi = "10.1016/j.tcs.2020.10.001",

language = "English",

volume = "847",

pages = "134--146",

journal = "Theoretical Computer Science",

issn = "0304-3975",

publisher = "Elsevier",

}

TY - JOUR

T1 - Computing branching distances with quantitative games

AU - Fahrenberg, Uli

AU - Legay, Axel

AU - Quaas, Karin

N1 - Funding Information: This author's work is supported by the Chaire ISC : Engineering Complex Systems – École Polytechnique Foundation – Thales – FX – DGA – Dassault Aviation – Naval Group – ENSTA Paris – Télécom Paris. Publisher Copyright: © 2020 Elsevier B.V.

PY - 2020/12/22

Y1 - 2020/12/22

N2 - We lay out a general method for computing branching distances between labeled transition systems. We translate the quantitative games used for defining these distances to other, path-building games which are amenable to methods from the theory of quantitative games. We then show for all common types of branching distances how the resulting path-building games can be solved. In the end, we achieve a method which can be used to compute all branching distances in the linear-time–branching-time spectrum.

AB - We lay out a general method for computing branching distances between labeled transition systems. We translate the quantitative games used for defining these distances to other, path-building games which are amenable to methods from the theory of quantitative games. We then show for all common types of branching distances how the resulting path-building games can be solved. In the end, we achieve a method which can be used to compute all branching distances in the linear-time–branching-time spectrum.

KW - Branching distance

KW - Path-building game

KW - Quantitative game

KW - Quantitative verification

UR - http://www.scopus.com/inward/record.url?scp=85092072665&partnerID=8YFLogxK

U2 - 10.1016/j.tcs.2020.10.001

DO - 10.1016/j.tcs.2020.10.001

M3 - Journal article

AN - SCOPUS:85092072665

SN - 0304-3975

VL - 847

SP - 134

EP - 146

JO - Theoretical Computer Science

JF - Theoretical Computer Science

ER -

Computing branching distances with quantitative games

Abstract

Bibliographical note

Keywords

Access to Document

AUB Link

Other files and links

Fingerprint

Cite this