Quantitative Simulation Games

Abstract. Classical formalizations of systems and properties are bool-ean: given a system and a property, the property is either true or false of the system. The classical view partitions the world into “correct ” and “incorrect ” systems, offering few nuances. In reality, of several systems that satisfy a property in the boolean sense, often some are more desir-able than others, and of the many systems that violate a property, usually some are less objectionable than others. For instance, among the systems that satisfy the response property that every request be granted, we may prefer systems that grant requests quickly (the quicker, the better), or we may prefer systems that issue few unnecessary grants (the fewer, the better); and among the systems that violate the response property, we may prefer systems that serve many initial requests (the more, the bet-ter), or we may prefer systems that serve many requests in the long run (the greater the fraction of served to unserved requests, the better). Formally, 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 be-tween a system and a property provides a measure of “fit ” or “desirabil-ity. ” 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 quan-titative objectives. In particular, for systems that satisfy a property, a quantitative simulation game can measure the “robustness ” of the sat-isfaction: how much can the system 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 vi-olation: how much does the property have to be modified so that it is satisfied by the system?