Dissertation/Thesis Abstract

Game relations, metrics and refinements
by Raman, Vishwanath, Ph.D., University of California, Santa Cruz, 2010, 294; 3421295
Abstract (Summary)

Game models for formal analysis have seen significant research effort over the last two decades. For the analysis of systems with non-deterministic behavior, games are a natural model of choice for studying both co-operative and competitive behaviors of the sources of non-determinism. In game models where the sources of non-determinism are treated adversarially, we have that the properties verified, or refinements synthesized, are correct against all possible realizations of non-deterministic behavior. In areas such as security protocols, where participants are rational and are primarily concerned with achieving their own objectives, and only secondarily concerned with violating the objectives of other participants, games are a natural model of participant behaviors. There is active ongoing research in both the theory and applications of games for verification, compositional reasoning and synthesis. In this dissertation, we first develop the theory of approximate behavioral equivalence and refinement in stochastic games and next explore games for synthesis in two different domains. The first in the automatic synthesis of fair non-repudiation protocols, a subclass of fair exchange protocols, used in e-commerce and the second in synthesizing resource managers that ensure progress, and hence lack of starvation, in multi-threaded C programs. Our results are derived from ideas in probabilistic systems, Markov decision processes and stochastic games.

Indexing (document details)
Advisor: Alfaro, Luca de
Commitee:
School: University of California, Santa Cruz
School Location: United States -- California
Source: DAI-B 71/09, Dissertation Abstracts International
Source Type: DISSERTATION
Subjects: Computer science
Keywords: Behavioral equivalence, Bisimulation, Game relations
Publication Number: 3421295
ISBN: 9781124203508
Copyright © 2019 ProQuest LLC. All rights reserved. Terms and Conditions Privacy Policy Cookie Policy
ProQuest