Linear and Branching System Metrics

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 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 micron-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 algorithm. for computing the distances over finite systems, together with matching lower complexity bounds.

Open PDF

Document Details

Document Type
Technical Report
Publication Date
Apr 08, 2005
Accession Number
ADA456691

Entities

People

  • Luca De Alfaro
  • Marco Faella
  • Marielle Stoelinga

Organizations

  • University of California, Santa Cruz

Tags

DTIC Thesaurus Topics

  • Abstracts
  • Algorithms
  • Availability
  • Calculus
  • California
  • Classification
  • Computers
  • Contracts
  • Engineering
  • Inclusions
  • Information Operations
  • Instructions
  • Monitoring
  • Security
  • Simulations
  • Simulators
  • Transitions

Readers

  • Computational Modeling and Simulation
  • Mathematical Modeling and Probability Theory.

Technology Areas

  • Space