Designing languages for expressing dependencies in strategic reasoning

Strategic reasoning is central to address behaviours of agents in a multi-agent system. It mainly relies on logic, used as a language for specifying properties. For instance, a designer of a system can write rich temporal properties, such as "two robots can reach a certain goal whatever a third robot is doing". Strategic reasoning tackles two main tasks: (1) automatic verification that a given multi-agent system fulfills some requirements (2) automatic synthesis of a multi-agent system that satisfies some requirements. In the last decade, many logical frameworks were proposed to reason about abilities of agents, among which the well-known ones of alternating-time temporal logic (ATL) and of strategy logic (SL).

Importantly, in a strategic environment, agents take decisions that *depend* on the behaviour of other agents. However, even very expressive logics (such as ATL and SL) cannot convey dependencies of agents' decisions in a precise manner; by default the current decision of a player depends on the entire strategies of the others they committed to, which is not realistic. On the contrary, dependencies like "the current decision of a player depends only on the last value chosen by another player" (alike the acknowledged Markov assumption in many modelling techniques) or "the current decision of a player depends on what other agents could have done" (alike threatening  in game theory) cannot be expressed.

The objective of the PhD is to design logical languages that make such dependencies explicit for strategic reasoning. Different approaches could be investigated in an attempt to face the trade-off between computational complexity of the language and its expressiveness. Usually the more expressive a logical language is, the more automatic verification and automatic synthesis problems are computationally difficult.

Technical challenges are many. There are algorithmic issues for verification and synthesis tasks. The investigations should identify the exact theoretical computational complexity of these tasks, provide algorithms and a way to implement them. Also, expressiveness properties of the proposed languages should be established as well as axiomatizing them.

An accurate examination of the literature displays weaknesses of the proposals. We site here two main approaches.

First, Hintikka and Sandu [1] proposed independence-friendly logic to specify dependencies of quantified variables ("exists x" and "forall x") on top of classic first-order logic. In formulas with nested quantifications, existentially quantified variables implicitly depend on all previous universally quantified variables: for instance, in an expression of the form "forall x forall y exists z ...", the value of variable z depends on both the values of x and y. On the contrary, in independence-friendly logic, variable dependencies are not induced by the quantification prefix in a linearly  manner, but rely on an explicit statement in the language: for example, in an expression of the form "forall x forall y exists z[x] ..." one requires that variable z only depends on x (and not on y). The more complex expression "forall x forall y exists z[x] exists w[y] ..."  cannot even be expressed in classic first-order logic.

Second, Mogavero et al. [2] and Gardy et al. [3] discussed a similar problem in dedicated logics for strategy dependencies. The semantics of these logics rely on a variant of Skolem functions (of first-order logic), called dependency maps. The developed setting is fairly complex, with a highly heavy mathematical machinery. additionally, as it does rely a finite syntactic representation, decision problems about such logics  (verification and synthesis tasks) are difficult to address in a simple manner.

We propose to approach strategy dependencies by means of circuits of transducers (input/output finite-state automata) in order to make explicit the dependencies: in this setting, the shape of a circuit reflects the dependencies between the strategies, while the transducers' type (e.g. as defined in [4]) reflects the information on the strategies of the others a player may use to select her response.

The expectation of this setting is to take advantage of the automata-theoretic approach.

The study will start with the simple framework of a game where players have to set a valuation of propositions on the linear order, that provides a semantics to an enriched version of Quantified Propositional Temporal Logic [5] with explicit dependencies. The adequate kind of transducers for this setting are transducers on infinite words. Then, one has to (1) investigate on designing a natural semantics of strategic logic statements with explicit dependencies between player strategies, and in particular on defining meaningful circuits of transducers on infinite words; (2) develop a novel manner to measure the complexity of dependencies requirements; (3) design effective methods for the verification and synthesis tasks.

Next, the study should turn to dealing with dependencies of strategies in general games arenas. Here, players have to set a valuation of propositions on (the unfolding of) the game arena. We may then resort to transducers on infinite trees. Questions similar to the case of the simple framework must also be answered.