
In twoplayer games on graphs, the players move a token through a graph to
produce an infinite path, which determines the winner or payoff of the game.
Such games are central in formal verification since they model the interaction
between a nonterminating system and its environment. We study {\em bidding
games} in which the players bid for the right to move the token. Two bidding
rules have been defined. In {\em Richman} bidding, in each round, the players
simultaneously submit bids, and the higher bidder moves the token and pays the
other player. {\em Poorman} bidding is similar except that the winner of the
bidding pays the "bank" rather than the other player. While poorman
reachability games have been studied before, we present, for the first time,
results on {\em infiniteduration} poorman games. A central quantity in these
games is the {\em ratio} between the two players' initial budgets. The
questions we study concern a necessary and sufficient ratio with which a player
can achieve a goal. For qualitative objectives such as parity, we show that the
properties of poorman games are largely similar to the properties of their
Richman counterparts. Our most interesting results concern poorman meanpayoff
games, where we construct optimal strategies depending on the ratio. Unlike in
the Richman case, where the optimal value is determined by the structure of the
game, in poorman bidding, with a higher ratio, a player can achieve a better
payoff. This is shown via a connection with probabilistic games, which in
itself is surprising, given that such a connection is not known for poorman
reachability games. We also solve the complexity problems that arise from these
games.

The edit distance between two words $w_1, w_2$ is the minimal number of word
operations (letter insertions, deletions, and substitutions) necessary to
transform $w_1$ to $w_2$. The edit distance generalizes to languages
$\mathcal{L}_1, \mathcal{L}_2$, where the edit distance from $\mathcal{L}_1$ to
$\mathcal{L}_2$ is the minimal number $k$ such that for every word from
$\mathcal{L}_1$ there exists a word in $\mathcal{L}_2$ with edit distance at
most $k$. We study the edit distance computation problem between pushdown
automata and their subclasses. The problem of computing edit distance to a
pushdown automaton is undecidable, and in practice, the interesting question is
to compute the edit distance from a pushdown automaton (the implementation, a
standard model for programs with recursion) to a regular language (the
specification). In this work, we present a complete picture of decidability and
complexity for the following problems: (1)~deciding whether, for a given
threshold $k$, the edit distance from a pushdown automaton to a finite
automaton is at most $k$, and (2)~deciding whether the edit distance from a
pushdown automaton to a finite automaton is finite.

Evolutionary graph theory studies the evolutionary dynamics in a population
structure given as a connected graph. Each node of the graph represents an
individual of the population, and edges determine how offspring are placed. We
consider the classical birthdeath Moran process where there are two types of
individuals, namely, the residents with fitness 1 and mutants with fitness r.
The fitness indicates the reproductive strength. The evolutionary dynamics
happens as follows: in the initial step, in a population of all resident
individuals a mutant is introduced, and then at each step, an individual is
chosen proportional to the fitness of its type to reproduce, and the offspring
replaces a neighbor uniformly at random. The process stops when all individuals
are either residents or mutants. The probability that all individuals in the
end are mutants is called the fixation probability. We present faster
polynomialtime MonteCarlo algorithms for finidng the fixation probability on
undirected graphs. Our algorithms are always at least a factor O(n^2/log n)
faster as compared to the previous algorithms, where n is the number of nodes,
and is polynomial even if r is given in binary. We also present lower bounds
showing that the upper bound on the expected number of effective steps we
present is asymptotically tight for undirected graphs.

In this paper we study how to play (stochastic) games optimally using little
space. We focus on repeated games with absorbing states, a type of twoplayer,
zerosum concurrent meanpayoff games. The prototypical example of these games
is the well known Big Match of Gillete (1957). These games may not allow
optimal strategies but they always have {\epsilon}optimal strategies. In this
paper we design {\epsilon}optimal strategies for Player 1 in these games that
use only O(log log T ) space. Furthermore, we construct strategies for Player 1
that use space s(T), for an arbitrary small unbounded nondecreasing function
s, and which guarantee an {\epsilon}optimal value for Player 1 in the limit
superior sense. The previously known strategies use space {\Omega}(logT) and it
was known that no strategy can use constant space if it is {\epsilon}optimal
even in the limit superior sense. We also give a complementary lower bound.
Furthermore, we also show that no Markov strategy, even extended with finite
memory, can ensure value greater than 0 in the Big Match, answering a question
posed by Abraham Neyman.

Balanced knockout tournaments are ubiquitous in sports competitions and are
also used in decisionmaking and elections. The traditional computational
question, that asks to compute a draw (optimal draw) that maximizes the winning
probability for a distinguished player, has received a lot of attention.
Previous works consider the problem where the pairwise winning probabilities
are known precisely, while we study how robust is the winning probability with
respect to small errors in the pairwise winning probabilities. First, we
present several illuminating examples to establish: (a)~there exist
deterministic tournaments (where the pairwise winning probabilities are~0 or~1)
where one optimal draw is much more robust than the other; and (b)~in general,
there exist tournaments with slightly suboptimal draws that are more robust
than all the optimal draws. The above examples motivate the study of the
computational problem of robust draws that guarantee a specified winning
probability. Second, we present a polynomialtime algorithm for approximating
the robustness of a draw for sufficiently small errors in pairwise winning
probabilities, and obtain that the stated computational problem is NPcomplete.
We also show that two natural cases of deterministic tournaments where the
optimal draw could be computed in polynomial time also admit polynomialtime
algorithms to compute robust optimal draws.

We study algorithmic questions for concurrent systems where the transitions
are labeled from a complete, closed semiring, and path properties are algebraic
with semiring operations. The algebraic path properties can model dataflow
analysis problems, the shortest path problem, and many other natural problems
that arise in program analysis. We consider that each component of the
concurrent system is a graph with constant treewidth, a property satisfied by
the controlflow graphs of most programs. We allow for multiple possible
queries, which arise naturally in demand driven dataflow analysis. The study of
multiple queries allows us to consider the tradeoff between the resource usage
of the onetime preprocessing and for each individual query. The traditional
approach constructs the product graph of all components and applies the
bestknown graph algorithm on the product. In this approach, even the answer to
a single query requires the transitive closure, which provides no room for
tradeoff between preprocessing and query time.
Our main contributions are algorithms that significantly improve the
worstcase running time of the traditional approach, and provide various
tradeoffs depending on the number of queries. For example, in a concurrent
system of two components, the traditional approach requires hexic time in the
worst case for answering one query as well as computing the transitive closure,
whereas we show that with onetime preprocessing in almost cubic time, each
subsequent query can be answered in at most linear time, and even the
transitive closure can be computed in almost quartic time. Furthermore, we
establish conditional optimality results showing that the worstcase running
time of our algorithms cannot be improved without achieving major breakthroughs
in graph algorithms.

We consider finitestate concurrent stochastic games, played by k>=2 players
for an infinite number of rounds, where in every round, each player
simultaneously and independently of the other players chooses an action,
whereafter the successor state is determined by a probability distribution
given by the current state and the chosen actions. We consider reachability
objectives that given a target set of states require that some state in the
target is visited, and the dual safety objectives that given a target set
require that only states in the target set are visited. We are interested in
the complexity of stationary strategies measured by their patience, which is
defined as the inverse of the smallest nonzero probability employed. Our main
results are as follows: We show that in twoplayer zerosum concurrent
stochastic games (with reachability objective for one player and the
complementary safety objective for the other player): (i) the optimal bound on
the patience of optimal and epsilonoptimal strategies, for both players is
doubly exponential; and (ii) even in games with a single nonabsorbing state
exponential (in the number of actions) patience is necessary. In general we
study the class of nonzerosum games admitting stationary epsilonNash
equilibria. We show that if there is at least one player with reachability
objective, then doublyexponential patience may be needed for epsilonNash
equilibrium strategies, whereas in contrast if all players have safety
objectives, the optimal bound on patience for epsilonNash equilibrium
strategies is only exponential.

We consider the core algorithmic problems related to verification of systems
with respect to three classical quantitative properties, namely, the
meanpayoff property, the ratio property, and the minimum initial credit for
energy property. The algorithmic problem given a graph and a quantitative
property asks to compute the optimal value (the infimum value over all traces)
from every node of the graph. We consider graphs with constant treewidth, and
it is wellknown that the controlflow graphs of most programs have constant
treewidth. Let $n$ denote the number of nodes of a graph, $m$ the number of
edges (for constant treewidth graphs $m=O(n)$) and $W$ the largest absolute
value of the weights. Our main theoretical results are as follows. First, for
constant treewidth graphs we present an algorithm that approximates the
meanpayoff value within a multiplicative factor of $\epsilon$ in time $O(n
\cdot \log (n/\epsilon))$ and linear space, as compared to the classical
algorithms that require quadratic time. Second, for the ratio property we
present an algorithm that for constant treewidth graphs works in time $O(n
\cdot \log (a\cdot b))=O(n\cdot\log (n\cdot W))$, when the output is
$\frac{a}{b}$, as compared to the previously best known algorithm with running
time $O(n^2 \cdot \log (n\cdot W))$. Third, for the minimum initial credit
problem we show that (i) for general graphs the problem can be solved in
$O(n^2\cdot m)$ time and the associated decision problem can be solved in
$O(n\cdot m)$ time, improving the previous known $O(n^3\cdot m\cdot \log
(n\cdot W))$ and $O(n^2 \cdot m)$ bounds, respectively; and (ii) for constant
treewidth graphs we present an algorithm that requires $O(n\cdot \log n)$ time,
improving the previous known $O(n^4 \cdot \log (n \cdot W))$ bound.

We study the problem of solving discounted, two player, turn based,
stochastic games (2TBSGs). Jurdzinski and Savani showed that 2TBSGs with
deterministic transitions can be reduced to solving $P$matrix linear
complementarity problems (LCPs). We show that the same reduction works for
general 2TBSGs. This implies that a number of interior point methods for
solving $P$matrix LCPs can be used to solve 2TBSGs. We consider two such
algorithms. First, we consider the unified interior point method of Kojima,
Megiddo, Noma, and Yoshise, which runs in time $O((1+\kappa)n^{3.5}L)$, where
$\kappa$ is a parameter that depends on the $n \times n$ matrix $M$ defining
the LCP, and $L$ is the number of bits in the representation of $M$. Second, we
consider the interior point potential reduction algorithm of Kojima, Megiddo,
and Ye, which runs in time $O(\frac{\delta}{\theta}n^4\log \epsilon^{1})$,
where $\delta$ and $\theta$ are parameters that depend on $M$, and $\epsilon$
describes the quality of the solution. For 2TBSGs with $n$ states and discount
factor $\gamma$ we prove that in the worst case $\kappa =
\Theta(n/(1\gamma)^2)$, $\delta = \Theta(\sqrt{n}/(1\gamma))$, and $1/\theta
= \Theta(n/(1\gamma)^2)$. The lower bounds for $\kappa$, $\delta$, and
$1/\theta$ are obtained using the same family of deterministic games.

Interprocedural analysis is at the heart of numerous applications in
programming languages, such as alias analysis, constant propagation, etc.
Recursive state machines (RSMs) are standard models for interprocedural
analysis. We consider a general framework with RSMs where the transitions are
labeled from a semiring, and path properties are algebraic with semiring
operations. RSMs with algebraic path properties can model interprocedural
dataflow analysis problems, the shortest path problem, the most probable path
problem, etc. The traditional algorithms for interprocedural analysis focus on
path properties where the starting point is \emph{fixed} as the entry point of
a specific method. In this work, we consider possible multiple queries as
required in many applications such as in alias analysis. The study of multiple
queries allows us to bring in a very important algorithmic distinction between
the resource usage of the \emph{onetime} preprocessing vs for \emph{each
individual} query. The second aspect that we consider is that the control flow
graphs for most programs have constant treewidth.
Our main contributions are simple and implementable algorithms that support
multiple queries for algebraic path properties for RSMs that have constant
treewidth. Our theoretical results show that our algorithms have small
additional onetime preprocessing, but can answer subsequent queries
significantly faster as compared to the current bestknown solutions for
several important problems, such as interprocedural reachability and shortest
path. We provide a prototype implementation for interprocedural reachability
and intraprocedural shortest path that gives a significant speedup on several
benchmarks.

We consider concurrent meanpayoff games, a very wellstudied class of
twoplayer (player 1 vs player 2) zerosum games on finitestate graphs where
every transition is assigned a reward between 0 and 1, and the payoff function
is the longrun average of the rewards. The value is the maximal expected
payoff that player 1 can guarantee against all strategies of player 2. We
consider the computation of the set of states with value 1 under finitememory
strategies for player 1, and our main results for the problem are as follows:
(1) we present a polynomialtime algorithm; (2) we show that whenever there is
a finitememory strategy, there is a stationary strategy that does not need
memory at all; and (3) we present an optimal bound (which is double
exponential) on the patience of stationary strategies (where patience of a
distribution is the inverse of the smallest positive probability and represents
a complexity measure of a stationary strategy).

We consider concurrent games played by twoplayers on a finitestate graph,
where in every round the players simultaneously choose a move, and the current
state along with the joint moves determine the successor state. We study a
fundamental objective, namely, meanpayoff objective, where a reward is
associated to each transition, and the goal of player 1 is to maximize the
longrun average of the rewards, and the objective of player 2 is strictly the
opposite. The path constraint for player 1 could be qualitative, i.e., the
meanpayoff is the maximal reward, or arbitrarily close to it; or quantitative,
i.e., a given threshold between the minimal and maximal reward. We consider the
computation of the almostsure (resp. positive) winning sets, where player 1
can ensure that the path constraint is satisfied with probability 1 (resp.
positive probability). Our main results for qualitative path constraints are as
follows: (1) we establish qualitative determinacy results that show that for
every state either player 1 has a strategy to ensure almostsure (resp.
positive) winning against all player2 strategies, or player 2 has a spoiling
strategy to falsify almostsure (resp. positive) winning against all player1
strategies; (2) we present optimal strategy complexity results that precisely
characterize the classes of strategies required for almostsure and positive
winning for both players; and (3) we present quadratic time algorithms to
compute the almostsure and the positive winning sets, matching the best known
bound of algorithms for much simpler problems (such as reachability
objectives). For quantitative constraints we show that a polynomial time
solution for the almostsure or the positive winning set would imply a solution
to a longstanding open problem (the value problem for turnbased deterministic
meanpayoff games) that is not known to be solvable in polynomial time.

We consider the problem of minimizing the regret in stochastic multiarmed
bandit, when the measure of goodness of an arm is not the mean return, but some
general function of the mean and the variance.We characterize the conditions
under which learning is possible and present examples for which no natural
algorithm can achieve sublinear regret.

We study twoplayer (zerosum) concurrent meanpayoff games played on a
finitestate graph. We focus on the important subclass of ergodic games where
all states are visited infinitely often with probability 1. The algorithmic
study of ergodic games was initiated in a seminal work of Hoffman and Karp in
1966, but all basic complexity questions have remained unresolved. Our main
results for ergodic games are as follows: We establish (1) an optimal
exponential bound on the patience of stationary strategies (where patience of a
distribution is the inverse of the smallest positive probability and represents
a complexity measure of a stationary strategy); (2) the approximation problem
lie in FNP; (3) the approximation problem is at least as hard as the decision
problem for simple stochastic games (for which NP intersection coNP is the
longstanding best known bound). We present a variant of the strategyiteration
algorithm by Hoffman and Karp; show that both our algorithm and the classical
valueiteration algorithm can approximate the value in exponential time; and
identify a subclass where the valueiteration algorithm is a FPTAS. We also
show that the exact value can be expressed in the existential theory of the
reals, and establish squareroot sum hardness for a related class of games.

Oneclock priced timed games is a class of twoplayer, zerosum,
continuoustime games that was defined and thoroughly studied in previous
works. We show that oneclock priced timed games can be solved in time m 12^n
n^(O(1)), where n is the number of states and m is the number of actions. The
best previously known time bound for solving oneclock priced timed games was
2^(O(n^2+m)), due to Rutkowski. For our improvement, we introduce and study a
new algorithm for solving oneclock priced timed games, based on the sweepline
technique from computational geometry and the strategy iteration paradigm from
the algorithmic theory of Markov decision processes. As a corollary, we also
improve the analysis of previous algorithms due to Bouyer, Cassez, Fleury, and
Larsen; and Alur, Bernadsky, and Madhusudan.

Markov decision processes (MDPs) and simple stochastic games (SSGs) provide a
rich mathematical framework to study many important problems related to
probabilistic systems. MDPs and SSGs with finitehorizon objectives, where the
goal is to maximize the probability to reach a target state in a given finite
time, is a classical and wellstudied problem. In this work we consider the
strategy complexity of finitehorizon MDPs and SSGs. We show that for all
$\epsilon>0$, the natural class of counterbased strategies require at most
$\log \log (\frac{1}{\epsilon}) + n+1$ memory states, and memory of size
$\Omega(\log \log (\frac{1}{\epsilon}) + n)$ is required. Thus our bounds are
asymptotically optimal. We then study the periodic property of optimal
strategies, and show a subexponential lower bound on the period for optimal
strategies.

For matrix games we study how small nonzero probability must be used in
optimal strategies. We show that for nxn winlosedraw games (i.e. (1,0,1)
matrix games) nonzero probabilities smaller than n^{O(n)} are never needed. We
also construct an explicit nxn winlose game such that the unique optimal
strategy uses a nonzero probability as small as n^{Omega(n)}. This is done by
constructing an explicit (1,1) nonsingular nxn matrix, for which the inverse
has only nonnegative entries and where some of the entries are of value
n^{Omega(n)}.

Gimbert and Horn gave an algorithm for solving simple stochastic games with
running time O(r! n) where n is the number of positions of the simple
stochastic game and r is the number of its coin toss positions. Chatterjee et
al. pointed out that a variant of strategy iteration can be implemented to
solve this problem in time 4^r r^{O(1)} n^{O(1)}. In this paper, we show that
an algorithm combining value iteration with retrograde analysis achieves a time
bound of O(r 2^r (r log r + n)), thus improving both time bounds. While the
algorithm is simple, the analysis leading to this time bound is involved, using
techniques of extremal combinatorics to identify worst case instances for the
algorithm.

Two standard algorithms for approximately solving twoplayer zerosum
concurrent reachability games are value iteration and strategy iteration. We
prove upper and lower bounds of 2^(m^(Theta(N))) on the worst case number of
iterations needed by both of these algorithms for providing nontrivial
approximations to the value of a game with N nonterminal positions and m
actions for each player in each position. In particular, both algorithms have
doublyexponential complexity. Even when the game given as input has only one
nonterminal position, we prove an exponential lower bound on the worst case
number of iterations needed to provide nontrivial approximations.