Simulation Distances

Boolean notions of correctness are formalized by preorders on systems. Quantitative measures of correctness can be formalized by realvalued distance functions between systems, where the distance between implementation and specification provides a measure of "fit" or "desirability." We extend the simulation preorder to the quantitative setting, by making each player of a simulation game pay a certain price for her choices. We use the resulting games with quantitative objectives to define three different simulation distances. The correctness distance measures how much the specification must be changed in order to be satisfied by the implementation. The coverage distance measures how much the implementation restricts the degrees of freedom offered by the specification. The robustness distance measures how much a system can deviate from the implementation description without violating the specification. We consider these distances for safety as well as liveness specific...

• Type: Conference
• Year: 2010
• Where: CONCUR
• Authors: Pavol Cerný, Thomas A. Henzinger, Arjun Radhakrishna
• Keywords: CONCUR 2010, Distance Functions, Distributed And Parallel Computing, Robustness Distance, Simulation Distances