A Generic Approach to Quantitative Verification
Uli Fahrenberg

TL;DR
This thesis develops a comprehensive, distance-based framework for quantitative verification of systems, enabling robust, compositional analysis independent of specific distance measures, and extends to quantitative specifications.
Contribution
It introduces a general, distance-agnostic theory of quantitative verification using game-based distances and extends to quantitative modal transition systems.
Findings
Defines various distances like bisimulation and simulation distances.
Constructs a quantitative generalization of the linear-time--branching-time spectrum.
Extends the theory to quantitative behavioral specifications.
Abstract
This thesis is concerned with quantitative verification, that is, the verification of quantitative properties of quantitative systems. These systems are found in numerous applications, and their quantitative verification is important, but also rather challenging. In particular, given that most systems found in applications are rather big, compositionality and incrementality of verification methods are essential. In order to ensure robustness of verification, we replace the Boolean yes-no answers of standard verification with distances. Depending on the application context, many different types of distances are being employed in quantitative verification. Consequently, there is a need for a general theory of system distances which abstracts away from the concrete distances and develops quantitative verification at a level independent of the distance. It is our view that in a theory of…
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.
Taxonomy
TopicsFormal Methods in Verification · Logic, programming, and type systems · Polynomial and algebraic computation
