arXiv subjects

Youssouf Oualhadj

Publications and source records attributed to Youssouf Oualhadj.

14 recordsLinked to original sources

arXiv2024

Deciding the synthesis problem for hybrid games through bisimulation

Hybrid games are games played on a finite graph endowed with real variables which may model behaviors of discrete controllers of continuous systems. The synthesis problem for hybrid games is decidable for classical objectives (like LTL formulas) when the games are initialized singular, meaning that the slopes of the continuous variables are piecewise constant and variables are reset whenever their slope changes. The known proof adapts the region construction from timed games. In this paper we show that initialized singular games can be reduced, via a sequence of alternating bisimulations, to timed games, generalizing the known reductions by bisimulation from initialized singular automata to timed automata. Alternating bisimulation is the generalization of bisimulation to games, accomodating a strategy translation lemma by which, when two games are bisimilar and carry the same observations, each strategy in one of the games can be translated to a strategy in the second game such that all the outcomes of the second strategy satisfies the same property that are satisfied by the first strategy. The advantage of the proposed approach is that one may then use realizability tools for timed games to synthesize a winning strategy for a given objective, and then use the strategy translation lemma to obtain a winning strategy in the hybrid game for the same objective.

cs.LO↗

arXiv2024

Fairness and promptness in Muller formulas

In this paper we consider two different views of the model checking problems for the Linear Temporal Logic (LTL). On the one hand, we consider the universal model checking problem for LTL, where one asks that for a given system and a given formula all the runs of the system satisfy the formula. On the other hand, the fair model checking problem for LTL asks that for a given system and a given formula almost all the runs of the system satisfy the formula. It was shown that these two problems have the same theoretical complexity i.e. PSPACE-complete. The question arises whether one can find a fragment of LTL for which the complexity of these two problems differs. One such fragment was identified in a previous work, namely the Muller fragment. We address a similar comparison for the prompt fragment of LTL (pLTL). pLTL extends LTL with an additional operator, i.e. the prompt-eventually. This operator ensures the existence of a bound such that liveness properties are satisfied within this bound. We show that the corresponding Muller fragment for pLTL does not enjoy the same algorithmic properties with respect to the comparison considered. We also identify a new expressive fragment for which the fair model checking is faster than the universal one.

cs.LO↗

arXiv2024

Controller Synthesis in Timed Büchi Automata: Robustness and Punctual Guards

We consider the synthesis problem on timed automata with Büchi objectives, where delay choices made by a controller are subjected to small perturbations. Usually, the controller needs to avoid punctual guards, such as testing the equality of a clock to a constant. In this work, we generalize to a robustness setting that allows for punctual transitions in the automaton to be taken by controller with no perturbation. In order to characterize cycles that resist perturbations in our setting, we introduce a new structural requirement on the reachability relation along an accepting cycle of the automaton. This property is formulated on the region abstraction, and generalizes the existing characterization of winning cycles in the absence of punctual guards. We show that the problem remains within PSPACE despite the presence of punctual guards.

cs.GT↗

arXiv2023

Arena-Independent Finite-Memory Determinacy in Stochastic Games

We study stochastic zero-sum games on graphs, which are prevalent tools to model decision-making in presence of an antagonistic opponent in a random environment. In this setting, an important question is the one of strategy complexity: what kinds of strategies are sufficient or required to play optimally (e.g., randomization or memory requirements)? Our contributions further the understanding of arena-independent finite-memory (AIFM) determinacy, i.e., the study of objectives for which memory is needed, but in a way that only depends on limited parameters of the game graphs. First, we show that objectives for which pure AIFM strategies suffice to play optimally also admit pure AIFM subgame perfect strategies. Second, we show that we can reduce the study of objectives for which pure AIFM strategies suffice in two-player stochastic games to the easier study of one-player stochastic games (i.e., Markov decision processes). Third, we characterize the sufficiency of AIFM strategies through two intuitive properties of objectives. This work extends a line of research started on deterministic games to stochastic ones.

cs.GT↗

arXiv2022

Careful Autonomous Agents in Environments With Multiple Common Resources

Careful rational synthesis was defined in (Condurache et al. 2021) as a quantitative extension of Fisman et al.'s rational synthesis (Fisman et al. 2010), as a model of multi-agent systems in which agents are interacting in a graph arena in a turn-based fashion. There is one common resource, and each action may decrease or increase the resource. Each agent has a temporal qualitative objective and wants to maintain the value of the resource positive. One must find a Nash equilibrium. This problem is decidable. In more practical settings, the verification of the critical properties of multi-agent systems calls for models with many resources. Indeed, agents and robots consume and produce more than one type of resource: electric energy, fuel, raw material, manufactured goods, etc. We thus explore the problem of careful rational synthesis with several resources. We show that the problem is undecidable. We then propose a variant with bounded resources, motivated by the observation that in practical settings, the storage of resources is limited. We show that the problem becomes decidable, and is no harder than controller synthesis with Linear-time Temporal Logic objectives.

cs.LO↗

arXiv2022

Games Where You Can Play Optimally with Arena-Independent Finite Memory

For decades, two-player (antagonistic) games on graphs have been a framework of choice for many important problems in theoretical computer science. A notorious one is controller synthesis, which can be rephrased through the game-theoretic metaphor as the quest for a winning strategy of the system in a game against its antagonistic environment. Depending on the specification, optimal strategies might be simple or quite complex, for example having to use (possibly infinite) memory. Hence, research strives to understand which settings allow for simple strategies. In 2005, Gimbert and Zielonka provided a complete characterization of preference relations (a formal framework to model specifications and game objectives) that admit memoryless optimal strategies for both players. In the last fifteen years however, practical applications have driven the community toward games with complex or multiple objectives, where memory -- finite or infinite -- is almost always required. Despite much effort, the exact frontiers of the class of preference relations that admit finite-memory optimal strategies still elude us. In this work, we establish a complete characterization of preference relations that admit optimal strategies using arena-independent finite memory, generalizing the work of Gimbert and Zielonka to the finite-memory case. We also prove an equivalent to their celebrated corollary of great practical interest: if both players have optimal (arena-independent-)finite-memory strategies in all one-player games, then it is also the case in all two-player games. Finally, we pinpoint the boundaries of our results with regard to the literature: our work completely covers the case of arena-independent memory (e.g., multiple parity objectives, lower- and upper-bounded energy objectives), and paves the way to the arena-dependent case (e.g., multiple lower-bounded energy objectives).

cs.GT↗

arXiv2020

Life is Random, Time is Not: Markov Decision Processes with Window Objectives

The window mechanism was introduced by Chatterjee et al. to strengthen classical game objectives with time bounds. It permits to synthesize system controllers that exhibit acceptable behaviors within a configurable time frame, all along their infinite execution, in contrast to the traditional objectives that only require correctness of behaviors in the limit. The window concept has proved its interest in a variety of two-player zero-sum games because it enables reasoning about such time bounds in system specifications, but also thanks to the increased tractability that it usually yields. In this work, we extend the window framework to stochastic environments by considering Markov decision processes. A fundamental problem in this context is the threshold probability problem: given an objective it aims to synthesize strategies that guarantee satisfying runs with a given probability. We solve it for the usual variants of window objectives, where either the time frame is set as a parameter, or we ask if such a time frame exists. We develop a generic approach for window-based objectives and instantiate it for the classical mean-payoff and parity objectives, already considered in games. Our work paves the way to a wide use of the window mechanism in stochastic models.

cs.LO↗

arXiv2018

Banach-Mazur Parity Games and Almost-sure Winning Strategies

Two-player stochastic games are games with two 2 players and a randomised entity called "nature". A natural question to ask in this framework is the existence of strategies that ensure that an event happens with probability 1 (almost-sure strategies). In the case of Markov decision processes, when the event 2 of interest is given as a parity condition, we can replace the "nature" by two more players that play according to the rules of what is known as Banach-Mazur game [1]. In this paper we continue this research program by extending the above result to two-player stochastic parity games. As in the paper [1], the basic idea is that, under the correct hypothesis, we can replace the randomised player with two players playing a Banach-Mazur game. This requires a few technical observations, and a non trivial proof, that this paper sets out to do.

cs.GT↗

arXiv2018

The Complexity of Concurrent Rational Synthesis

In this paper, we investigate the rational synthesis problem for concurrent game structure for a variety of objectives ranging from reachability to Muller condition. We propose a new algorithm that establishes the decidability of the non cooperative rational synthesis problem that relies solely on game theoretic technique as opposed to previous approaches that are logic based. Thanks to this approach, we construct a zero-sum turn-based game that can be adapted to each one of the afore mentioned objectives thus obtain new complexity results. In particular, we show that reachability, safety, Büchi, and co-Büchi conditions are PSpace-complete, Muller, Street, and Rabin are PSpace-hard and in ExpTime.

cs.LO↗

arXiv2017

Two Recursively Inseparable Problems for Probabilistic Automata

This paper introduces and investigates decision problems for numberless probabilistic automata, i.e. probabilistic automata where the support of each probabilistic transitions is specified, but the exact values of the probabilities are not. A numberless probabilistic automaton can be instantiated into a probabilistic automaton by specifying the exact values of the non-zero probabilistic transitions. We show that the two following properties of numberless probabilistic automata are recursively inseparable: - all instances of the numberless automaton have value 1, - no instance of the numberless automaton has value 1.

cs.FL↗

arXiv2016

Rational Verification in Iterated Electric Boolean Games

Electric boolean games are compact representations of games where the players have qualitative objectives described by LTL formulae and have limited resources. We study the complexity of several decision problems related to the analysis of rationality in electric boolean games with LTL objectives. In particular, we report that the problem of deciding whether a profile is a Nash equilibrium in an iterated electric boolean game is no harder than in iterated boolean games without resource bounds. We show that it is a PSPACE-complete problem. As a corollary, we obtain that both rational elimination and rational construction of Nash equilibria by a supervising authority are PSPACE-complete problems.

cs.GT↗

arXiv2015

Deciding the value 1 problem for probabilistic leaktight automata

The value 1 problem is a decision problem for probabilistic automata over finite words: given a probabilistic automaton, are there words accepted with probability arbitrarily close to 1? This problem was proved undecidable recently; to overcome this, several classes of probabilistic automata of different nature were proposed, for which the value 1 problem has been shown decidable. In this paper, we introduce yet another class of probabilistic automata, called leaktight automata, which strictly subsumes all classes of probabilistic automata whose value 1 problem is known to be decidable. We prove that for leaktight automata, the value 1 problem is decidable (in fact, PSPACE-complete) by constructing a saturation algorithm based on the computation of a monoid abstracting the behaviours of the automaton. We rely on algebraic techniques developed by Simon to prove that this abstraction is complete. Furthermore, we adapt this saturation algorithm to decide whether an automaton is leaktight. Finally, we show a reduction allowing to extend our decidability results from finite words to infinite ones, implying that the value 1 problem for probabilistic leaktight parity automata is decidable.

cs.FL↗

arXiv2012

Deciding the Value 1 Problem of Probabilistic Leaktight Automata

The value 1 problem is a decision problem for probabilistic automata over finite words: given a probabilistic automaton A, are there words accepted by A with probability arbitrarily close to 1? This problem was proved undecidable recently. We sharpen this result, showing that the undecidability result holds even if the probabilistic automata have only one probabilistic transition. Our main contribution is to introduce a new class of probabilistic automata, called leaktight automata, for which the value 1 problem is shown decidable (and PSPACE-complete). We construct an algorithm based on the computation of a monoid abstracting the behaviours of the automaton, and rely on algebraic techniques developed by Simon for the correctness proof. The class of leaktight automata is decidable in PSPACE, subsumes all subclasses of probabilistic automata whose value 1 problem is known to be decidable (in particular deterministic automata), and is closed under two natural composition operators.

cs.FL↗

arXiv2011

Pushing undecidability of the isolation problem for probabilistic automata

This short note aims at proving that the isolation problem is undecidable for probabilistic automata with only one probabilistic transition. This problem is known to be undecidable for general probabilistic automata, without restriction on the number of probabilistic transitions. In this note, we develop a simulation technique that allows to simulate any probabilistic automaton with one having only one probabilistic transition.

cs.FL↗