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

    74 Citations (Scopus)
    64 Downloads (Pure)


    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
    Issue number2
    Publication statusPublished - Mar 2009


    • 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