Automata-based Quantitative Verification

Quantitative analysis of computing systems is an emerging area in automated formal analysis. Such properties address aspects such as costs and rewards, quality measures, resource consumption, distance metrics, etc. Existing solutions for problems in quantitative analysis face two challenges, namely lack of generalizability and separation-of-techniques. Lack of generalizability refers to the issue that solution approaches are specialized to cost model. Different cost models deploy such disparat...