In this paper we revisit the paradigm shift “From Boolean to Quantitative Notions of Correctness” proposed by Henzinger more than 10 years ago. In particular, we present the notion of Convex Lattice Equation Systems as a universal framework for encoding and inferring behavioural metrics between quantitative system behaviours. We demonstrate how the framework may be applied to infer bounds on values of stochastic games and distances between timed systems.
|Title of host publication||Principles of Systems Design : Essays Dedicated to Thomas A. Henzinger on the Occasion of His 60th Birthday|
|Number of pages||18|
|Publication status||Published - 2022|
|Series||Lecture Notes in Computer Science (LNCS)|