Last updated on 7 June.
K. Apt. Stable partitions in coalitional games
D. Berwanger. Backwards Induction for Games of Infinite Horizon
T. Colcombet. Ramseyan factorisation for trees
J. Duparc. Towards the Wadge Hierarchy of Weak Alternating Tree Automata
J. Esparza. Solving fixpoint equations in omega-continuous semirings: Some ideas and many questions
K. Etessami. Recursive Concurrent Stochastic Games
S. Fröschle. When is secrecy decidable?
H. Gimbert. Positional Stochastic Games
N. Immerman. On Size versus Number of Variables
D. Janin. On distributed synthesis of discrete systems
B. Jonsson. Proving Liveness by Backwards Reachability
M. Jurdzinski. Optimality equations and strategy improvement for average payoff games
M. Lange. Model Checking Games for Fixpoint Logic with Chop
R. Lazic. On LTL with the freeze quantifier and register automata
A. Murawski. Game semantics and automata
J. Obdrzalek. Are Parity Games Spineless?
T. Touili. Verifying Concurrent Message-Passing C Programs with Recursive Calls
Y. Venema. Coalgebra automata
S. Vorobyov. Are One-Player Games Always Simple?
I. Walukiewicz. Tree algebras
W. Zielonka. From discounting to parity games
V. Barany. A hierarchy of automatically presentable omega-words having a decidable MSO theory
F. Horn. Finitary Parity and Streett Games
L. Kaiser. Game Quantification on Automatic Structures and Hierarchical Games
P. Krcal. Communicating Timed Automata
S. Lasota. Faster Algorithm for Bisimulation Equivalence of Normed Context-Free Processes
K. Y. Rozier. Algorithms for Automata-Theoretic Linear Temporal Logic Model Checking
M. Samuelides. Pebble tree-walking automata
A. Trivedi A strategy improvement algorithm for optimal time reachability games
We propose a notion of a stable partition in a coalitional game that is parametrized by the concept of a defection function. This function assigns to each partition of the grand coalition a set of different coalition arrangements for a group of defecting players. The alternatives are compared using their social welfare.
We characterize the stability of a partition for a number of most natural defection functions and investigate whether and how so defined stable partitions can be reached from any initial partition by means of simple transformations.
The approach is illustrated by analyzing an example in which a set of stores seeks an optimal transportation arrangement. (Joint work with Tadeusz Radzik)
One of the most important open problems in mathematical optimization is the existence of a strongly polynomial algorithm for linear programming. In the polynomial ellipsoid algorithm due to Khachiyan and the interior-point algorithms of Karmarkar, the number of operations depends not only on the dimensions of the system of constraints, but also on the magnitude of the coefficients. The quest for an algorithm with a running time polynomial in the number of variables and constraints while independent of the coefficients, has continued for the last quarter of a century.
Particular cases of this fundamental open problem appear in solving infinite games. For instance, the only currently known way to efficiently solve the one-player version of Shapley's stochastic games [Shapley 1953] (or Markov decision processes) is by solving a linear program. However, this program has many special properties. The constraints are monotonic with coefficients between 0 and 1, and the feasible region contains a unique maximal element, which is also the solution to the game. Furthermore, the function mapping pure positional strategies to payoffs possesses the following useful combinatorial properties.
Although there are strongly subexponential and non-strongly polynomial algorithms, the existence of a strongly polynomial algorithm is an important open problem. Looking attractive and feasible, investigating it seems to be a natural step toward the general problem.
We report on a recent progress that has been achieved in the particular case of discounted payoff games [Andersson 2006, Andersson Svensson Vorobyov 2006]. By adapting the existing algorithms for feasibility testing, it was demonstrated that one-player generalized discounted payoff games can be solved in strongly polynomial time. When combined with the general combinatorial optimization schemes of [Bjorklund Vorobyov, TCS 2005], this also yields the currently best known strongly subexponential algorithm for the two-player version of discounted payoff games. We also present new geometric and combinatorial algorithms that solve one-player discounted games (in strongly polynomial time) and simple stochastic games (in hopefully strongly polynomial time).
We investigate automatic presentations of omega-words. Starting point of our study is the work of Carton and Thomas on the decidability of the MSO theory of morphic words. Refining their technique we show that the length-lexicographic presentation of a (morphic) word is canonical in a certain sense, implying that the class of morphic words is closed under d.g.s.m. mappings, which seems to be a new result. We then go on to generalize our method to a hierarchy of classes of infinite words enjoying the above mentioned properties. We introduce $k$-lexicographic presentations, and morphisms of level $k$ stacks and show that these are inter-translatable, and thus give rise to the same classes of $k$-lexicographic or level $k$ morphic words. A number of other equivalent characterizations are given. We prove that the $k$-lexicographic presentations are also canonical, implying closure of each of these classes under d.g.s.m. mappings, and decidability of the MSO theory of all words representable in any of these forms. The classes of $k$-lexicographic words are shown to form a strictly increasing infinite hierarchy.
Predictions of Nash Equilibrium in sequential games are renown to be seldom realistic. One standard method to overcome this problem in games of finite horizon is backwards induction: handle the simplest subgames first, and then proceed inductively until the original game is solved.
We propose a backwards-induction technique for infinite games on finite graphs. Our setting is non-zero-sum, and involves two or more players with omega-regular objectives. Building on the notion of iterated admissibility, i.e., avoidance of weakly dominated strategies, we argue that this generalisation of backwards induction is algorithmically sound, and discuss some of its properties.
We consider the model-checking problem for C programs with (1) data ranging over very large domains, (2) (recursive) procedure calls, and (3) concurrent parallel components that communicate via synchronizing actions. We model such programs using communicating pushdown systems, and reduce the reachability problem for this model to deciding the emptiness of the intersection of two context-free languages L1 and L2. We tackle this undecidable problem using a CounterExample Guided Abstraction Refinement (CEGAR) scheme. We implemented our technique in the model checker MAGIC and found a previously unknown bug in a version of a Windows NT Bluetooth driver.
Ramsey's theorem is the key tool used by Buchi for complementing the so-called buchi automata without any form of determinisation. Complementing techniques for Rabin/parity tree-automata uses a radically different approach; parity games.
We consider in this talk an alternative approach to this last result via a lemma showing the existence of a form of Ramseyan decomposition for trees. This approach is more ressemblant to the original proof of Buchi.
Temporal logics, first-order logics, and automata over data words have recently attracted considerable attention. A data word is a word over a finite alphabet, together with a piece of data (an element of an infinite domain) at each position. Examples include timed words and XML documents. To refer to the data, temporal logics are extended with the freeze quantifier (equivalently, predicate $\lambda$-abstraction); first-order logics with predicates over the data domain; and automata with registers or pebbles.
We investigate relative expressiveness and complexity of standard decision problems for LTL with the freeze quantifier (LTL$^\downarrow$), 2-variable first-order logic (FO$^2$) over data words, and register automata. The only predicate available on data is equality. Previously undiscovered connections among LTL$^\downarrow$, register automata and counter systems with incrementation errors enable us to answer several questions left open in recent literature.
We show that the future-time fragment of LTL$^\downarrow$ which corresponds to FO$^2$ over finite data words can be exteded considerably while preserving decidability, but at the expense of non-primitive recursive complexity, and that most further extensions are undecidable. We also prove that surprisingly, over infinite data words, LTL$^\downarrow$ with only X and F operators, as well as universality of one-way nondeterministic register automata, are undecidable even when there is only 1 register.
We consider alternating tree automata with weak parity acceptance condions. This means that, given any state $q$, the priority of all accessible states from $q$ is at least the one of $q$. And the acceptation or rejection of infinite binary trees relies on the existence of a winning strategy for one of the two players in a parity game. We show that the language recognized by such an automaton with priorities in $[0,n]$ is $\Pi^0_n$, and in $[1,n+1]$ is $\Sigma^0_n$. We show that the Wadge Hierarchy of these languages not only contains complete sets for all finite differences of $\Pi^0_n$ and $\Sigma^0_n$ sets, but much more since the whole hierarchy has length at least $(\omega^\omega)^\omega$. Hence, much higher that the Wadge hierarchy of deterministic tree languages unearthed by Filip Murlak.
Monotonic systems of equations in omega-continuous semirings are introduced. After some motivation, we consider the problem of finding iteration schemes for the solution. We present some known results for particular cases, one or two small new results, and many open questions.
This is work in progress with Stefan Kiefer and Michael Luttenberger.
We study Recursive Concurrent Stochastic Games (RCSGs), extending our recent analysis of recursive simple stochastic games [EY05c,EY06] to a concurrent setting where the two players choose moves simultaneously and independently at each state. For multi-exit games, our earlier work already showed undecidability for basic questions like termination, thus we focus on the important case of single-exit RCSGs (1-RCSGs).
We first characterize the value of a 1-RCSG termination game as the least fixed point solution of a system of nonlinear minimax functional equations, and use it to show PSPACE decidability for the quantitative termination problem. We then give a strategy improvement technique, which we use to show that player 1 (maximizer) has epsilon-optimal randomized Stackless & Memoryless (r-SM) strategies, while player 2 (minimizer) has optimal r-SM strategies. Thus, such games are r-SM-determined. These results mirror and generalize in a strong sense the randomized memoryless determinacy results for finite stochastic games, and extend the classic Hoffman-Karp [HK66] strategy improvement approach from the finite to an infinite state setting. The proofs in our infinite-state setting are very different however, relying on subtle analytic properties of certain power series that arise from studying 1-RCSGs.
We show that our upper bounds, even for qualitative termination, can not be improved without a major breakthrough, by giving two reductions: first a P-time reduction from the long-standing square-root sum problem to the quantitative termination decision problem for *finite* concurrent stochastic games, and then a P-time reduction from the latter problem to the qualitative termination problem for 1-RCSGs.
Joint work with Mihalis Yannakakis (Columbia U.), based on a paper that will appear at ICALP'06.
The hope to be able to validate cryptographic protocols automatically seems to have been thwarted by the fact that most security properties such as secrecy have turned out to be undecidable. On the other hand, one could argue that the undecidability proofs exhibited so far do leave room for positive results: most of these proofs exploit properties of the formal models used to represent protocols rather than characteristics possessed by `realistic protocols'. In this talk I will discuss ongoing research whose goal is to characterize natural classes of protocols with decidable security properties.
We study zero-sum perfect information stochastic payoff games with finitely many states. We focuse our attention on the existence of positional optimal strategies, i.e. optimal strategies which do not use memory. In the first part of this talk we focuse on the case where there is only one player; such a game is often called a Markov decision process. We introduce the class of convex payoff functions and prove that any Markov decision process equiped with a convex payoff function admits positional optimal strategies.
In the second part of this talk, we present a theorem that reduce the positionality of two player games to the positionality of Markov decision processes. Then we show how to use those results for proving quickly traditional positionality results, as well as new ones.
Part of this work is joint work with Wieslaw Zielonka.
Parity conditions and Streett/Rabin conditions are central in games theory.
There are two main versions of these games: The so-called "weak" ones deal with the set of occuring states, while the classical games deal with the set of states occuring infinitely often.
Between these two models, Chaterjee and Henzinger defined a hybrid way, called "finitary". As in classical games, "bad" events (odd priorities or requests) that occur finitely often are not considered. But for those bad events that occur infinitely often, the corresponding good event (smaller even priority or corresponding answer) must occur after a bounded delay. Chatterjee and Henzinger proved that these games are determined for parity and Streett winning conditions, and proposed algorithms to compute winning regions and strategies.
We present here a faster way to solve such finitary games. We solve finitary parity in polynomial time (O(n³)), and finitary Streett in time O(4^k*k^2*n²*m²).
In LICS 2001, Adler and I used a variant of Ehrenfeucht-Fraisee games to prove lower bounds on the size of first-order formulas rather than their quantifier-depth. In LICS 2004, Grohe and Schweikardt used a related approach to investigate the relationship between size and number of variables in formulas describing linear orders. I will explain this area and describe some work in progress with my student, Philipp Weis, concerning the size/variable trade-off.
We give an overview of various results in the field of distributed synthesis of discrete systems and examine several directions of research that shall be investigated further more.
We present a new method for proving liveness and termination properties for fair concurrent programs, which does not rely on finding a ranking function orx on computing the transitive closure of the transition relation. The set of states from which termination or some liveness property is guaranteed is computed by a backwards reachability analysis. A central tools is a check for a certain commutativity property. The method is not complete. Its power can be extended by repeated applications, and by extending the transition relation (as in abstraction). It can also be seen as a complement to other methods for proving termination, in that it transforms a termination problem into a simpler one with a larger set of terminated states. We show the usefulness of our method by applying it to existing programs from the literature. We have also implemented it in the framework of Regular Model Checking, and used it to automatically verify non-starvation for infinite-state and parameterized algorithms.
Joint work with Parosh Abdulla, Ahmed Rezine, Mayank Saksena.
In an average payoff game two players, Min and Max, construct an infinite path by taking turns to move a token along an edge of a graph in which every vertex has an integer payoff. Player Min wants to minimize the limit of average payoffs along the path and player Max wants to maximize it.
This talk complements existing literature on average payoff games on finite graphs by formulating optimality equations whose solutions yield optimal strategies. It also introduces a natural strategy improvement algorithm for solving optimality equations. The algorithm generalizes classical policy iteration algorithms for Markov decision processes and yields an alternative proof of positional determinacy for average payoff games. Natural generalizations of optimality equations for infinite state average payoff games will be also discussed.
Game quantification is an expressive concept and has been studied in model theory and descriptive set theory, especially in relation to infinitary logics. Automatic structures on the other hand play an important role in computer science, especially in program verification. We extend first-order logic on structures on words by allowing to use an infinite string of alternating quantifiers on letters of a word, the game quantifier. This extended logic is decidable and preserves regularity on automatic structures, but can be undecidable on other structures even with decidable first-order theory. We show that in the presence of game quantifier any relation that allows to distinguish successors is enough to define all regular relations and therefore the game quantifier is strictly more expressive than first-order logic in such cases.
Conversely, if there is an automorphism of atomic relations that swaps some successors then we prove that it can be extended to any relations definable with game quantifier. After investigating it's expressiveness, we use game quantification to introduce a new type of combinatorial games with multiple players and imperfect information exchanged with respect to a hierarchical constraint. It is shown that these games on finite arenas exactly capture the logic with game quantifier when players alternate their moves but are undecidable and not necessarily determined in the other case.
We study channel systems whose behaviour (sending and receiving messages via unbounded FIFO channels) must follow given timing constraints specifying the execution speeds of the local components. We propose Communicating Timed Automata (CTA) to model such systems. The goal is to study the borderline between decidable and undecidable classes of channel systems in the timed setting. Our technical results include: (1) CTA with one channel without shared states in the form $(A_1,A_2, c_{1,2})$ is equivalent to one-counter machine, implying that verification problems such as checking state reachability and channel boundedness are decidable, and (2) CTA with two channels without sharing states in the form $(A_1,A_2,A_3, c_{1,2},c_{2,3})$ has the power of Turing machines. Note that in the untimed setting, these systems are no more expressive than finite state machines. The capability of synchronizing on time makes it substantially more difficult to verify channel systems.
In this talk we present two different model checking games for Fixpoint Logic with Chop - an extension of the modal mu-calculus with a sequential composition operator. We concentrate on explaining the winning conditions in these games, but also survey their (known) complexity results and applications.
The fastest known algorithm for checking bisimulation equivalence of normed context-free processes worked in $O(n^{13})$ time. We give an alternative algorithm working in $O(n^8 \polylog\ n)$ and $O(n^2\;v)$ time, where $v$ is the maximum norm of a process. As a side effect we improve the best known upper bound for testing equivalence of simple (deterministic) context-free grammars from $O(n^7 \polylog\ n)$ to $O(n^6 \polylog\ n)$. This is a joint work with Wojciech Rytter, Warsaw University.
In the past decade game semantics has emerged as a successful paradigm in semantics of programming languages. Its precision and concreteness have recently inspired a new approach to program analysis based on automata-theoretic representations of game models. In this talk we give an overview of this programme, focussing on relationships between game semantics and various classes of automata.
We present a new algorithm (actually two algorithms, but they have much in common) for solving parity games. The algorithm is based on the notion of spine, a structural way of capturing the (possible) winning sets and counter-strategies. The definition of spine and the algorithms were inspired by the strategy improvement algorithm, but there are important differences. For one, we do not start with an arbitrary strategy for one of the players, but with computing the `obvious' starting strategies. Second, in our algorithm we do not perform arbitrary improvement steps. Instead we try to get rid of winning cycles by (hopefully temporarily) making the associated measure worse. Third, we tried to give an algorithm which is symmetric, i.e. which allows us to make improvement steps for both the players in alternation.
This is joint work with Colin Stirling.
Numerous tools have been developed to translate LTL formulas into automata and check them against a system model. Some tools explicitly create an automaton from a given LTL formula, which can then be checked by a model-checking tool such as SPIN. Other tools, like SMV, specify the automaton symbolically, rather then explicitly. We can test the efficiency and the quality of these translations by testing for satisfiability of the LTL formulas. We will present benchmark data comparing ten such tools, examine their shortcomings, and consider the question: Can we do better?
Two variants of pebble tree-walking automata are considered that were introduced in the literature. It is shown that for each number of pebbles, the two models have the same expressive power both in the deterministic case and in the nondeterministic case. Furthermore, nondeterministic (resp. deterministic) tree-walking automata with n+1 pebbles can recognize more languages than those with n pebbles. Moreover, there is a regular tree language that is not recognized by any tree-walking automaton with pebbles. As a consequence, FO+posTC is strictly included in MSO over trees.
Efficient complementation of non-deterministic Buechi automata is essential for the automata-theoretic approach to the problem of program verification. This work presents an empirical comparison between explicit and symbolic implementations of the Kupferman-Vardi complementation algorithm by considering automaton universality as a model-checking problem. A novel encoding presented here allows the problem to be solved symbolically via a model-checker. We compare the performance of an explicit-search (SPIN) and of a symbolic-search (SMV) model-checkers on randomly generated automata based on a probabilistic framework introduced previously. We compare these results to the performance of an explicit-encoding explicit-search complementation tool (Wring) on the same set of automata. Finally, we present empirical results on the probability of randomly generating universal automata as a function of transition density, final-state density, and automaton size.
In an optimal time reachability game player Min (resp. Max) choses her moves so that the time to reach a given target configuration in a timed automaton is minimised (maximised). A value iteration based algorithm was proposed by Asarin and Maler in 1999 to compute epsilon-optimal strategies for both players. This talk complements their work by providing a strategy improvement algorithm for these games.
In this talk we introduce optimality equations, whose solutions give epsilon-optimal strategies for both players in an optimal time reachability game. In order to solve these equations effectively, we introduce the thin region abstraction which for every configuration has a finite number of symbolic timed moves. Then we present a strategy improvement algorithm which solves optimality equations for the thin optimal time reachability game.
Many of the most fundamental concepts and results in automata theory have a natural existence at a fairly high level of abstraction, viz. that of coalgebra. In the talk I introduce the notion of a coalgebra automaton, which generalizes automata that operate on words, trees or (amorphous) graphs. I motivate the concept and mention some of the most important results obtained so far.
With the help of $\mu$-calculus, a recent paper of de Alfaro, Henzinger and Majumdar (ICALP 2003) explores links between discounted and parity games. Using techniques from game theory and from Markov decision processes we examine these links in the special case of finite state stochastic perfect information games. We exhibit a family of partially discounted games with optimal positional strategies spanning from discounted games to parity games.
Joint work with Hugo Gimbert.
We present an algebraic framework for regular languages of finite unranked trees. The main idea is to use a well-known notion of transformation semigroup to recognize tree languages. This observation allows us to use notions of semigroup theory, such as wreath product, to study tree languages. We make connection between standard algebraic concepts such as aperiodicity, idempotency, commutativity, and definability in first-order logic, chain logic, CTL* and PDL. The obtained characterisations do not, however, yield decidability results.
Joint work with Mikolaj Bojanczyk.