Quantitative Simulation Games Book Section


Author(s): Cerný, Pavol; Henzinger, Thomas A; Radhakrishna, Arjun
Article/Chapter Title: Quantitative Simulation Games
Title Series: LNCS
Affiliation IST Austria
Abstract: While a boolean notion of correctness is given by a preorder on systems and properties, a quantitative notion of correctness is defined by a distance function on systems and properties, where the distance between a system and a property provides a measure of “fit” or “desirability.” In this article, we explore several ways how the simulation preorder can be generalized to a distance function. This is done by equipping the classical simulation game between a system and a property with quantitative objectives. In particular, for systems that satisfy a property, a quantitative simulation game can measure the “robustness” of the satisfaction, that is, how much the system can deviate from its nominal behavior while still satisfying the property. For systems that violate a property, a quantitative simulation game can measure the “seriousness” of the violation, that is, how much the property has to be modified so that it is satisfied by the system. These distances can be computed in polynomial time, since the computation reduces to the value problem in limit average games with constant weights. Finally, we demonstrate how the robustness distance can be used to measure how many transmission errors are tolerated by error correcting codes.
Keywords: correctness; quantitative games; quantitative verification; robustness; simulation
Book Title: Time For Verification: Essays in Memory of Amir Pnueli
Volume: 6200
ISBN: 978-3642137532
Publisher: Springer  
Publication Place: Berlin, Heidelberg
Date Published: 2010-07-29
Start Page: 42
End Page: 60
Sponsor: This work was partially supported by the European Union project COMBEST and the European Network of Excellence ArtistDesign.
DOI: 10.1007/978-3-642-13754-9_3
Open access: no
IST Austria Authors
  1. Thomas A. Henzinger
    415 Henzinger
  2. Pavol Černý
    25 Cerný
Related IST Austria Work