Show simple item record

dc.contributor.advisor Vardi, Moshe Y
dc.creatorBansal, Suguman
dc.date.accessioned 2020-08-14T18:37:35Z
dc.date.available 2020-08-14T18:37:35Z
dc.date.created 2020-08
dc.date.issued 2020-05-13
dc.date.submitted August 2020
dc.identifier.citation Bansal, Suguman. "Automata-Based Quantitative Verification." (2020) Diss., Rice University. https://hdl.handle.net/1911/109208.
dc.identifier.urihttps://hdl.handle.net/1911/109208
dc.description.abstract The analysis of quantitative properties of computing systems, or quantitative analysis in short, is an emerging area in automated formal analysis. Such properties address aspects such as costs and rewards, quality measures, resource consumption, distance metrics, and the like. So far, several applications of quantitative analysis have been identified, including formal guarantees for reinforcement learning, planning under resource constraints, and verification of (multi-agent) on-line economic protocols. Existing solution approaches for problems in quantitative analysis suffer from two challenges that adversely impact the theoretical understanding of quantitative analysis, and large-scale applicability due to limitations on scalability. These are the lack of generalizability, and {separation-of-techniques. Lack of generalizability refers to the issue that solution approaches are often specialized to the underlying cost model that evaluates the quantitative property. Different cost models deploy such disparate algorithms that there is no transfer of knowledge from one cost model to another. Separation-of-techniques refers to the inherent dichotomy in solving problems in quantitative analysis. Most algorithms comprise of two phases: A structural phase, which reasons about the structure of the quantitative system(s) using techniques from automata or graphs; and a numerical phase, which reasons about the quantitative dimension/cost model using numerical methods. The techniques used in both phases are so unlike each other that they are difficult to combine, forcing the phases to be performed sequentially, thereby impacting scalability. This thesis contributes towards a novel framework that addresses these challenges. The introduced framework, called comparator automata or comparators in short, builds on automata-theoretic foundations to generalize across a variety of cost models. The crux of comparators is that they enable automata-based methods in the numerical phase, hence eradicating the dependence on numerical methods. In doing so, comparators are able to integrate the structural and numerical phases. On the theoretical front, we demonstrate that comparator-based solutions have the advantage of generalizable results, and yield complexity-theoretic improvements over a range of problems in quantitative analysis. On the practical front, we demonstrate through empirical analysis that comparator-based solutions render more efficient, scalable, and robust performance, and hold the ability to integrate quantitative with qualitative objectives.
dc.format.mimetype application/pdf
dc.language.iso eng
dc.subjectFormal methods
Quantiative verification and synthesis
Quantitative properties
Comparator automata
Quantitative inclusion
Quantitative games
Discounted-sum
dc.title Automata-Based Quantitative Verification
dc.type Thesis
dc.date.updated 2020-08-14T18:37:35Z
dc.type.material Text
thesis.degree.department Computer Science
thesis.degree.discipline Engineering
thesis.degree.grantor Rice University
thesis.degree.level Doctoral
thesis.degree.name Doctor of Philosophy
thesis.degree.major Formal methods


Files in this item

Thumbnail

This item appears in the following Collection(s)

Show simple item record