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 -