Luca de Alfarounread,
Jan 24, 2008, 7:02:14 PM1/24/08
to UCSC CS Theory and Software
CS 280G Talk:
Solving Games via Three-Valued Abstraction Refinement
Pritam Roy, UCSC
Monday January 28, 2008
Games that model realistic systems can have very large state-spaces,
making their direct solution difficult. We present a symbolic
abstraction-refinement approach to the solution of two-player games.
Given a property, an initial set of states, and a game representation,
our approach starts by constructing a simple abstraction of the game,
guided by the predicates present in the property and in the initial
set. The abstraction is then refined, until it is possible to either
prove, or disprove, the property over the initial states.
Specifically, we evaluate the property on the abstract game in
three-valued fashion, computing an over-approximation (the "may"
states), and an under-approximation (the "must" states), of the states
that satisfy the property. If this computation fails to yield a
certain yes/no answer to the validity of the property on the initial
states, our algorithm refines the abstraction by splitting uncertain
abstract states (states that are may-states, but not must-states).
The approach lends itself to an efficient symbolic implementation. We
discuss the property required of the abstraction scheme in order to
achieve convergence and termination of our technique. We present the
results for reachability and safety properties, as well as for fully
general omega-regular properties.