Krishnendu Chatterjee, Thomas Henzinger and Nir Piterman will receive one of the two CONCUR 2026 Test-of-Time Awards at CONCUR 2026. Those colleagues kindly agreed to answer some questions of mine on their award-winning paper via email. You can find their answers to my questions below. I hope you'll enjoy reading them as much as I did. Thanks, Krishnendu, Nir and Tom!
Luca: You receive the CONCUR ToT Award 2026 for your paper Strategy Logic, which appeared at CONCUR 2007 and, in archival form, in Information and Computation. In that article, you introduced a seminal logic for expressing properties of strategies over two-player games on graphs. Could you briefly explain to our readers what the main features of strategy logic are? Could you also tell us how you came to study the question addressed in your award-winning article? Which of the results in your paper did you find most surprising or challenging?
Krishnendu, Nir and Tom (henceforth abbreviated to KNT): The defining feature of Strategy Logic is that it treats strategies as explicit, first-class objects: strategies are named by variables, and the logic can quantify over them. Our main motivation was to express central concepts from game theory, such as equilibria, within a logical framework for games on graphs. As for the results, what we find most appealing is that a logic this expressive still admits decidability, and that several natural fragments come with clean and reasonable computational complexity. Establishing these decidability and complexity results for various fragments was also the most technically challenging part of the work.
Luca: With the benefit of hindsight, having a logic to describe properties of games that treats strategies as first-class objects sounds like an extremely natural idea. However, previous logics such as ATL, ATL*, the alternating-time µ-calculus and game logic followed a different path. Do you recall how you came to the realisation that treating strategies explicitly was the "way to go"?
KNT: One of the key application areas for graph games has been reactive synthesis, and until 2004 reactive synthesis was studied primarily as an adversarial game. Hence logics such as ATL, ATL*, alternating-time µ-calculus, and game logic, all focus on strictly competitive or cooperative behaviors of game theory. Around 2004-2005, we started working on connections between algorithmic game theory and graph games. As a consequence we considered aspects of Nash equilibria and other not strictly competitive notions of game theory (such as secure equilibria) in graph games. A natural question was to build a logical framework that can express these aspects of game theory, which led to Strategy Logic. In fact we first isolated the one-alternation fragment, which suffices to express these equilibria, and only afterwards arrived at the full, more expressive logic. In hindsight, the shift to treating strategies explicitly was driven by the questions we were asking rather than by a single eureka moment.
Luca: Strategy logic builds on LTL, which is a very natural choice, IMHO. Did you consider defining a version of strategy logic basing it on the (linear-time) modal μ--calculus? Would it be worth doing so and how would such a logic relate to the alternating-time μ-calculus?
KNT: There is always a tension between LTL and stronger formalisms that can recognize all ω-regular languages. Following the tradition of ATL and ATL*, we naturally chose to go with LTL for defining the (linear-time) objectives of players. As the techniques that we developed were automata based, it was clear that extensions of LTL that can express all ω-regular languages would be handled by the same techniques. The exact choice of the linear-time formalism (for example, ETL, QLTL, LDL, or the linear-time μ-calculus) is not very important as long as it can be readily translated to automata. In the alternating-time μ-calculus, however, by carefully nesting fixpoints and coalition quantification, we can define infinitely many changes of strategic context. But only in a completely adversarial manner.
Luca: As you are hinting, in your paper, amongst other results, you showed that the alternating-time μ-calculus and strategy logic have incomparable expressive power. Would a fixed-point version of strategy logic, based on the modal μ-calculus, be a way of achieving a logic that offers the "best of both worlds" while maintaining some of the good computational properties of strategy logic? Has anyone worked on such a logic?
KNT: We did not consider such a version of Strategy Logic. Intuitively, both classical and alternating-time μ-calculi combine local, single-transition branching operators such as Pre with fixpoint operators, whereas strategies express global behavioral choices and the objectives of players are defined on outcomes that are linear paths. An important expressive difference between the alternating-time μ-calculus and Strategy Logic is therefore due to the distinction between branching and linear time.
It seems interesting to consider a logic that would combine two types of pre operators: those that continue exploring pre-defined strategies and their induced behaviors and those that allow to change the strategic context starting a new behavioral exploration. But we believe that the techniques that handle alternating-time mu-calculus would work for such a logic and the mix of behavior and control might be very hard to understand.
Luca: Did you or anyone else ever implement the model-checking algorithms you present in your award-winning paper? If the answer is negative, do you think that there would still be interest in such a model checker and in its experimental evaluation?
KNT: As far as we know there is no full implementation of Strategy Logic. In general, we have very good implementations supporting the manipulation and analysis of automata on infinite words (such as Spot and Owl). They are also used as a basis for creating tools that solve reactive synthesis. But we do not have good tool support for using automata on infinite trees, which would be required in order to fully support Strategy Logic. The community studying Multi-Agent Systems adopted Strategy Logic and they have some support for the analysis of some questions. There are implementations of equilibrium checking and rational synthesis in the tool Eve that is developed in the group of Michael Wooldridge in Oxford. They support the analysis of concurrent game structures for such questions. There is also a restricted version of an epistemic extension of Strategy Logic that is included in the model checker MCMAS for Multi-Agent Systems, which was developed in the group of Alessio Lomuscio in Imperial College London.
MCMAS also supports ATL model checking and, in principle, it is possible to reduce the one-alternation fragment of Strategy Logic to ATL model checking, but we are not aware of this having been implemented.
Luca: You mentioned the uptake of strategy logic by the multi-agent systems community. How is strategy logic relevant and did you think that this work would be relevant to multi-agent systems?
KNT: Strategy Logic answered a natural need in Multi-Agent Systems research. For MAS, questions about the goals of agents and hence strategies are very natural. Many questions relate to rational behavior: whether agents have an incentive to follow a protocol, stability of behavior, what can coalitions do, and whether individuals can profitably deviate. The way Strategy Logic puts strategies in the center as explicit objects makes it very natural to study these questions.
We wouldn’t say that we saw it coming, but the signs of early adoption of strategic reasoning by the MAS community were already there. The uptake of ATL and ATL* started in the early 2000s and by 2004-2005 people were using it regularly. We are also very happy that some of the major developments of Strategy Logic came from this community.
Luca: Are there any problems that you left open in your award-winning article that you'd still love to see solved? Did you or any colleagues study the problem of "strategy synthesis"?
KNT: Definitely. For the complete logic, our paper established only a non-elementary upper bound and left the matching lower bound open. This gap was later closed by colleagues, who proved a matching non-elementary lower bound and thereby settled the computational complexity of the full logic. We also concentrated on the case of two-player games rather than multi-player games. The interaction between the logic and the game structure means that the two-player framework, in a sense, already captures the complexity of the logic. Indeed, the same techniques based on tree automata were later used by others to extend the logic to the multi-player setting (and concurrent game structures).
Luca: I am interested in how research collaborations start, as I like to tell "research-life stories" to PhD students and young researchers of all ages. Could you tell us how you started your collaboration on the award-winning paper?
KNT: The collaboration grew naturally out of a question from Tom (Thomas Henzinger): could notions such as the equilibria we had been studying be expressed in ATL or ATL*, and if not, what would be a natural and concise logic that could express them? Pursuing this led us to the one-alternation fragment. We then realized that strategies can be viewed as trees, which meant tree automata were the right tool — and Nir (Nir Piterman) was our automata expert. So the paper really came together at the meeting point of three ingredients: the study of non-zero-sum games, the wish for a logical framework to express their concepts, and tree-automata techniques.
Luca: How did the results and the techniques you developed in your award-winning paper influence your subsequent research? Is there any result obtained by other researchers that builds on your work and that you like in particular?
KNT: The result had a lasting influence. The interplay between games and automata that we exploited in the paper fed directly into later lines of work. e.g., from the connection of games and automata the notion of good-for-games (a.k.a. history-deterministic) automata emerged. Among the results by others that build on Strategy Logic, the matching non-elementary lower bound and the work on special classes of strategies — such as the distinction between behavioral and non-behavioral strategies — are very elegant.
Luca: To my mind, games on graphs ought to be viewed as one of the unifying themes within TCS, bridging the Volume A-Volume B divide, and I am happy to see that there is a
book-length treatment covering the subject now. What is your view on this matter? What impact do you think that your work has had, if any, on the community working on algorithmic game theory, broadly construed? (I am reminded of the
slides for a, typically thought-provoking, talk delivered by Moshe Vardi.) What has our community learnt from the work done in the field of computational game theory? And what, if anything, did they learn from the work done within the concurrency theory community?
KNT: Indeed, games on graphs is one of the unifying themes between Volume A and Volume B: it connects with logic and automata theory from Vol. B, and it connects with the notion of alternation from complexity theory and graph algorithms from Vol. A. The inflow of ideas from algorithmic game theory, or game theory in general, is a key source of ideas in this work, e.g., to express equilibria in a logical framework. Other notions of equilibria have also been studied in the context of reactive synthesis (e.g., rational synthesis), and Vol. B researchers have explored many concepts from general game theory beyond strictly competitive games. The broad area of algorithmic game theory also benefited from logical reasoning grounded in concurrency theory, e.g., Strategy Logic is the key logic for reasoning about behaviors in Multi-Agent Systems, and axiomatic characterizations for reasoning about strategy spaces have been influential in evolutionary game theory. There is also work using Strategy Logic in mechanism design.
Luca: What are the research topics related to logics for games on graphs that you find most interesting right now?
KNT: We can think of several interesting open questions: (i) the relationship between games and automata through the lens of history-determinism and similar concepts is an exciting direction; (ii) algorithmic bounds for several fundamental problems remain open, e.g., a polynomial-time algorithm for parity games; (iii) the degree to which sources of randomness can be shared between different players is an active area of research in concurrent games; and (iv) the study of computationally efficient logics which lie between ATL* and Strategy Logic is also under-explored.
Luca: What advice would you give to a young researcher who is keen to start working on topics related to logics for games and other computational problems related to games?
KNT: The rapid progress in AI makes this question a difficult one. We believe that formal methods in general will become a central part of computing, more than they have ever been, because AI-generated software needs checks even more than software written by humans, but even more so, because modern AI can, for the first time, provide or at least support such checks on a scale that was hitherto impossible. Formal checks do not necessarily have to take the form of, say, Lean proofs, but they could also include state-based reasoning involving automata and games. It is always difficult to predict the future, but finding the right place for our field in this future seems a uniquely exciting opportunity.
