arXiv subjects

Nathalie Bertrand

Publications and source records attributed to Nathalie Bertrand.

3 recordsLinked to original sources

arXiv2026

Antichains for Concurrent Parameterized Games (Long Version)

Concurrent parameterized games involve a fixed yet arbitrary number of players. They are described by finite arenas in which the edges are labeled with languages that describe the possible move combinations leading from one vertex to another (n players yield a word of length n). Previous work showed that, when edge labels are regular languages, one can decide whether a distinguished player, called Eve, has a strategy to ensure a reachability objective, against any strategy profile of her arbitrarily many opponents. This decision problem is known to be PSPACE-complete. A basic ingredient in the PSPACE-membership proof is the reduction to the exponential-size knowledge game, a 2-player game that reflects the knowledge Eve has on the number of opponents. In this paper, we provide a symbolic approach, based on antichains, to compute Eve's winning region in the knowledge game. In words, it gives the minimal knowledge Eve needs at every vertex to win the concurrent parameterized reachability game. More precisely, we propose two fixed-point algorithms that compute, as an antichain, the maximal elements of the winning region for Eve in the knowledge game. We implemented these two algorithms in C++, as well as the one initially proposed, and report on their relative performances on various benchmarks.

cs.LO↗

arXiv2026

Target Discounted Sum Problem on Markov Chains with Applications to Markov Decision Processes

The discounted sum is a way to aggregate a sequence of weights from a finite alphabet $Σ$, i.e., for a discount factor $λ$, the discounted sum of a sequence $w_0 w_1 w_2 \cdots$ over $Σ$ is $\sum_{i \in \mathbb{N}} w_i λ^i$. The target discounted-sum problem, which is currently open, asks, given $λ,Σ$ and a target $t$, whether there exists an infinite sequence over $Σ$ whose discounted sum is equal to $t$. We study and solve a probabilistic variant of this problem, i.e., the target discounted-sum problem on Markov chains. To do this, we prove that the event consisting of paths whose discounted sum is equal to the target and has infinitely many distinct suffix sums has probability zero. This structural property allows us to solve the target discounted-sum problem on Markov chains using an automata-theoretic technique. We apply our technical results to Markov decision processes with target discounted-sum objectives: we show that the infimum value and the finite-memory supremum value are computable in pseudo-polynomial time and are attained by deterministic finite-memory strategies.

cs.LO↗

arXiv2026

Reaching as Cheap as Possible in 1-clock Robust Weighted Timed Games

The value problem for 2-player games on graph generally consists in determining the minimal value Min can ensure against any possible strategy for Max. We consider here the value problem for reachability objectives in weighted timed games (WTGs) under a robust semantics. WTGs are a modelling formalism combining real-time constraints and integer weights on transitions and locations in an adversarial setting. Robustness allows for representing timing imprecisions in the measurement of delays and clock values. Robust weighted timed games have been introduced more than a decade ago: they are undecidable in general, and were quite recently shown decidable for the subclasses of acyclic or divergent robust WTGs. This paper pursues the goal of identifying decidable subclasses and establishes the decidability of the robust value problem for 1-clock WTGs.

cs.GT↗