Linear and Branching System Metrics
| Autor: | J., Hilston, de Alfaro, Luca, Faella, Marco, M.Z., Kwiatkowska, Telek, M., Stoelinga, Mariëlle Ida Antoinette |
|---|---|
| Přispěvatelé: | L., de Alfaro, Faella, Marco, M., Stoelinga |
| Rok vydání: | 2009 |
| Předmět: |
Pure mathematics
Computer science Process calculus 0102 computer and information sciences 02 engineering and technology 01 natural sciences Boolean algebra metrics symbols.namesake EC Grant Agreement nr.: FP7/214755 Computer Science::Logic in Computer Science Formal language 0202 electrical engineering electronic engineering information engineering EWI-16577 Temporal logic Equivalence (formal languages) Boolean function Equivalence (measure theory) Bisimulation Modal logic Linear system simulation METIS-264177 Specification techniques Metric space Logics of programs TheoryofComputation_MATHEMATICALLOGICANDFORMALLANGUAGES 010201 computation theory & mathematics TheoryofComputation_LOGICSANDMEANINGSOFPROGRAMS symbols 020201 artificial intelligence & image processing IR-68677 EC Grant Agreement nr.: IST-004527 EC Grant Agreement nr.: FP7-ICT-2007-1 Algorithm Software |
| Zdroj: | IEEE transactions on software engineering, 35(2):10.1109/TSE.2008.106, 258-273. IEEE |
| ISSN: | 1939-3520 0098-5589 |
| DOI: | 10.1109/tse.2008.106 |
| Popis: | 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 mu-calculus. We show that, while trace inclusion (respectively, equivalence) coincides with simulation (respectively, 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. |
| Databáze: | OpenAIRE |
| Externí odkaz: |
|