Synthesis with Rational Environments
====================================

Synthesis is the automated construction of a system from its
specification.  The system has to satisfy its specification in all
possible environments.  The environment often consists of agents that
have objectives of their own.  Thus, it makes sense to soften the
universal quantification on the behavior of the environment and take
the objectives of its underlying agents into an account.  Fisman et
al. introduced {\em rational synthesis}: the problem of synthesis in
the context of rational agents. The input to the problem consists of
temporal-logic formulas specifying the objectives of the system and
the agents that constitute the environment, and a solution concept
(e.g., Nash equilibrium).  The output is a profile of strategies, for
the system and the agents, such that the objective of the system is
satisfied in the computation that is the outcome of the strategies,
and the profile is stable according to the solution concept; that is,
the agents that constitute the environment have no incentive to
deviate from the strategies suggested to them.

In this paper we continue to study rational synthesis.  First, we
suggest an alternative definition to rational synthesis, in which the
agents are rational but not cooperative.  In the non-cooperative
setting, one cannot assume that the agents that constitute the
environment take into account the strategies suggested to them.
Accordingly, the output is a strategy for the system only, and the
objective of the system has to be satisfied in all the compositions
that are the outcome of a stable profile in which the system follows
this strategy.  We show that rational synthesis in this setting is
2\ExpTimeC, thus it is not more complex than traditional synthesis or
cooperative rational synthesis.  Second, we study a richer
specification formalism, where the objectives of the system and the
agents are not Boolean but quantitative.  In this setting, the goal of
the system and the agents is to maximize their outcome.  The
quantitative setting significantly extends the scope of rational
synthesis, making the game-theoretic approach much more relevant.