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 proceedingConference contributionAcademicpeer-review

    53 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 languageEnglish
    Title of host publicationAutomata, Languages and Programming
    Subtitle of host publication31st International Colloquium, ICALP 2004, Turku, Finland, July 12-16, 2004. Proceedings
    EditorsJ. Díaz, J. Karhumäki, A. Lepistö, D. Sannella
    Place of PublicationBerlin
    PublisherSpringer
    Pages97-109
    ISBN (Electronic)978-3-540-27836-8
    ISBN (Print)978-3-540-22849-3
    DOIs
    Publication statusPublished - 12 Jul 2004
    Event31st International Colloquium on Automata, Languages and Programming, ICALP 2004 - Turku University, Turku, Finland
    Duration: 12 Jul 200416 Jul 2004
    Conference number: 31
    http://www.math.utu.fi/projects/icalp2004/

    Publication series

    NameLecture Notes in Computer Science
    PublisherSpringer
    Volume3142
    ISSN (Print)0302-9743
    ISSN (Electronic)1611-3349

    Workshop

    Workshop31st International Colloquium on Automata, Languages and Programming, ICALP 2004
    Abbreviated titleICALP
    CountryFinland
    CityTurku
    Period12/07/0416/07/04
    Internet address

      Fingerprint

    Keywords

    • METIS-221392

    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). Berlin: Springer. https://doi.org/10.1007/978-3-540-27836-8_11