Tags:Abstract interpretation, Counter machines and Sequential decision making
Abstract:
In this extended abstract, we summarize our recent work on the efficient synthesis of sequential decision-making agents that optimize statistical properties such as maximum and average response times. In the setting of sequential decision-making, the environment is modeled as a random process that generates inputs. The agent responds to each input, aiming to maximize rewards and minimize costs within a specified time horizon. The corresponding synthesis problem is known to be PSPACE-hard in general. We consider the special case where the input distribution, reward, and cost depend on input-output statistics specified by counter automata. For such problems, we introduce the notion of statistical abstraction, which clusters statistically indistinguishable input- output sequences into equivalence classes. Using statistical abstractions, we present the first PTIME synthesis algorithms for such problems.
Abstraction-Based Decision Making for Statistical Properties