Dylan Bellier

Highlights Conference 2023 Conference Abstract

Plan Logic

• Dylan Bellier

Strategy logics has two major flaws: the decision problems associated have a high complexity (model checking is non elementary and satisfiability is undecidable) and the strategy quantified might not be feasible. However, these drawbacks appear to be related as the fragment One Goal has a 2-EXPTIME complexity and feasible strategies suffice to verify a formula. In this work, we propose an approach to define a logic suited to reason about feasible strategies by changing the domain of quantification. We replace strategies with plans (sequences of actions) and define a behavioral compositional semantics to ensure feasibility. This allows for the definition of an equivalent game-theoretic semantics and then, 2-EXPTIME decision procedures. Contributed talk given by Dylan Bellier

LAMAS&SR Workshop 2022 Workshop Paper

Dependency matrices for multiplayer strategic dependencies

• Dylan Bellier
• Sophie Pinchinat
• Francois Schwarzentruber

Highlights Conference 2022 Conference Abstract

Dependency Matrices: Multi-player Delay Games

• Dylan Bellier

Players in a game take their decisions with respect to their knowledge of what the other players do, or have done or even in some cases, will do. The study of temporal dependencies requires specific formalism through Delay games: two players play a classical Gale-Stewart game but the moves of one player are delayed. In this presentation, we propose a formalism generalizing Delay games, Dependency Matrices, for a multi-player setting. We solve the problem of the existense of a winning uniform strategy when all delays are finite and show that this problem is undecidable when delays may be infinite. We then propose a fragment to recover decidability that we call perfectible information. We solve the problem on this fragment by unifying Büchi automaton complemention and parity-game resolution.

LAMAS&SR Workshop 2021 Workshop Paper

DQPTL: Dependency Quantified Propositional Linear-time Temporal Logic

• Dylan Bellier
• Sophie Pinchinat
• François Schwarzentruber

We present an approach to specify the information flow between players in a concurrent game with LTL objectives. We use a dependency matrix D to reflect this information flow. On this basis, we define the so-called Dependency Quantified Propositional Linear-time Temporal Logic (DQPTL) whose for® where D is a dependency matrix, mulae are of the form D∃𝑝𝜑, ∃𝑝® informs which players form the coalition and 𝜑 is an LTL formula, whose semantics is a concurrent game. We show that our setting captures the standard semantics of Quantified Propositional Linear-time Temporal Logic (QPTL), for some adequate matrices D. Moreover, we provide an effective criterion to decide if a DQPTL formula is consistent in the sense that the concurrent game yields an entire labeling of the time line, so that the winning condition 𝜑 can be evaluated.

Highlights Conference 2021 Conference Abstract

Good-for-Game QPTL: An Alternating Hodges Semantics

• Dylan Bellier

An extension of QPTL is considered where functional dependencies among the quantified variables can be restricted in such a way that their current values are independent of the future values of the other variables. This restriction is tightly connected to the notion of behavioral strategies in game-theory and allows the resulting logic to naturally express game-theoretic concepts. The fragment where only restricted quantifications are considered, called behavioral quantifications, and can be decided, for both model checking and satisfiability, in 2ExpTime and is expressively equivalent to QPTL, though significantly less succinct.