Author name cluster

Thomas Brihaye

Possible papers associated with this exact author name in Arrow. This page groups case-insensitive exact name matches and is not a full identity disambiguation profile.

17 papers

2 author rows

GandALF Workshop 2022 Workshop Paper

Adversarial Formal Semantics of Attack Trees and Related Problems

Thomas Brihaye
Sophie Pinchinat
Alexandre Terefenko

Security is a subject of increasing attention in our actual society in order to protect critical resources from information disclosure, theft or damage. The informal model of attack trees introduced by Schneier, and widespread in the industry, is advocated in the 2008 NATO report to govern the evaluation of the threat in risk analysis. Attack-defense trees have since been the subject of many theoretical works addressing different formal approaches. In 2017, M. Audinot et al. introduced a path semantics over a transition system for attack trees. Inspired by the later, we propose a two-player interpretation of the attack-tree formalism. To do so, we replace transition systems by concurrent game arenas and our associated semantics consist of strategies. We then show that the emptiness problem, known to be NP-complete for the path semantics, is now PSPACE-complete. Additionally, we show that the membership problem is coNP-complete for our two-player interpretation while it collapses to P in the path semantics.

PDF Details DOI

I&C Journal 2022 Journal Article

Decisiveness of stochastic systems and its application to hybrid models

Patricia Bouyer
Thomas Brihaye
Mickael Randour
Cédric Rivière
Pierre Vandenhove

In 2007, Abdulla et al. introduced the concept of decisiveness, an interesting tool for lifting good properties of finite Markov chains to denumerable ones. Later, this concept was extended to more general stochastic transition systems (STSs), allowing the design of various verification algorithms for large classes of (infinite) STSs. We further improve the understanding and utility of decisiveness in two ways. First, we provide a general criterion for proving the decisiveness of general STSs. This criterion, which is very natural but whose proof is rather technical, (strictly) generalizes all known criteria from the literature. Second, we focus on stochastic hybrid systems (SHSs), a stochastic extension of hybrid systems. We establish the decisiveness of a large class of SHSs and, under a few classical hypotheses from mathematical logic, we show how to decide reachability problems in this class, even though they are undecidable for general SHSs. This provides a decidable stochastic extension of o-minimal hybrid systems.

Details DOI

I&C Journal 2021 Journal Article

Constrained existence problem for weak subgame perfect equilibria with ω-regular Boolean objectives

Thomas Brihaye
Véronique Bruyère
Aline Goeminne
Jean-François Raskin

We study multiplayer turn-based games played on a finite directed graph such that each player aims at satisfying an ω-regular Boolean objective. Instead of the well-known notions of Nash equilibrium (NE) and subgame perfect equilibrium (SPE), we focus on the recent notion of weak subgame perfect equilibrium (weak SPE), a refinement of SPE. In this setting, players who deviate can only use the subclass of strategies that differ from the original one on a finite number of histories. We are interested in the constrained existence problem for weak SPEs. We provide a complete characterization of the computational complexity of this problem: it is P-complete for Explicit Muller objectives, NP-complete for Co-Büchi, Parity, Muller, Rabin, and Streett objectives, and PSPACE-complete for Reachability and Safety objectives (we only prove NP-membership for Büchi objectives). We also show that the constrained existence problem is fixed parameter tractable and is polynomial when the number of players is fixed. All these results are based on a fine-grained analysis of a fixpoint algorithm that computes the set of possible payoff profiles underlying weak SPEs.

Details DOI

GandALF Workshop 2020 Workshop Paper

Decisiveness of Stochastic Systems and its Application to Hybrid Models

Patricia Bouyer
Thomas Brihaye
Mickael Randour
Cédric Rivière
Pierre Vandenhove

In [ABM07], Abdulla et al. introduced the concept of decisiveness, an interesting tool for lifting good properties of finite Markov chains to denumerable ones. Later, this concept was extended to more general stochastic transition systems (STSs), allowing the design of various verification algorithms for large classes of (infinite) STSs. We further improve the understanding and utility of decisiveness in two ways. First, we provide a general criterion for proving decisiveness of general STSs. This criterion, which is very natural but whose proof is rather technical, (strictly) generalizes all known criteria from the literature. Second, we focus on stochastic hybrid systems (SHSs), a stochastic extension of hybrid systems. We establish the decisiveness of a large class of SHSs and, under a few classical hypotheses from mathematical logic, we show how to decide reachability problems in this class, even though they are undecidable for general SHSs. This provides a decidable stochastic extension of o-minimal hybrid systems. [ABM07] Parosh A. Abdulla, Noomene Ben Henda, and Richard Mayr. 2007. Decisive Markov Chains. Log. Methods Comput. Sci. 3, 4 (2007).

PDF Details DOI

I&C Journal 2020 Journal Article

On the termination of dynamics in sequential games

Thomas Brihaye
Gilles Geeraerts
Marion Hallet
Stéphane Le Roux

We consider n-player non-zero sum games played on finite trees (i. e. , sequential games), in which the players have the right to repeatedly update their respective strategies. This generates a dynamics in the game which may eventually stabilise to a Nash Equilibrium, and we study the conditions that guarantee such a dynamics to terminate. We build on the works of Le Roux and Pauly who have studied the Lazy Improvement Dynamics. We extend these works by first defining a turn-based dynamics, proving that it terminates on subgame perfect equilibria, and showing that several variants do not terminate. Second, we define a variant of Kukushkin's lazy improvement where the players may now form coalitions to change strategies. We show how properties of the players' preferences on the outcomes affect the termination of this dynamics, and we characterise classes of games where it always terminates (in particular two-player games).

Details DOI

GandALF Workshop 2018 Workshop Paper

Constrained Existence Problem for Weak Subgame Perfect Equilibria with ω-Regular Boolean Objectives

Thomas Brihaye
Véronique Bruyère
Aline Goeminne
Jean-François Raskin

We study multiplayer turn-based games played on a finite directed graph such that each player aims at satisfying an omega-regular Boolean objective. Instead of the well-known notions of Nash equilibrium (NE) and subgame perfect equilibrium (SPE), we focus on the recent notion of weak subgame perfect equilibrium (weak SPE), a refinement of SPE. In this setting, players who deviate can only use the subclass of strategies that differ from the original one on a finite number of histories. We are interested in the constrained existence problem for weak SPEs. We provide a complete characterization of the computational complexity of this problem: it is P-complete for Explicit Muller objectives, NP-complete for Co-Büchi, Parity, Muller, Rabin, and Streett objectives, and PSPACE-complete for Reachability and Safety objectives (we only prove NP-membership for Büchi objectives). We also show that the constrained existence problem is fixed parameter tractable and is polynomial when the number of players is fixed. All these results are based on a fine analysis of a fixpoint algorithm that computes the set of possible payoff profiles underlying weak SPEs.

PDF Details DOI

GandALF Workshop 2017 Workshop Paper

Dynamics and Coalitions in Sequential Games

Thomas Brihaye
Gilles Geeraerts
Marion Hallet
Stéphane Le Roux

We consider N-player non-zero sum games played on finite trees (i. e. , sequential games), in which the players have the right to repeatedly update their respective strategies (for instance, to improve the outcome wrt to the current strategy profile). This generates a dynamics in the game which may eventually stabilise to a Nash Equilibrium (as with Kukushkin's lazy improvement), and we argue that it is interesting to study the conditions that guarantee such a dynamics to terminate. We build on the works of Le Roux and Pauly who have studied extensively one such dynamics, namely the Lazy Improvement Dynamics. We extend these works by first defining a turn-based dynamics, proving that it terminates on subgame perfect equilibria, and showing that several variants do not terminate. Second, we define a variant of Kukushkin's lazy improvement where the players may now form coalitions to change strategies. We show how properties of the players' preferences on the outcomes affect the termination of this dynamics, and we thereby characterise classes of games where it always terminates (in particular two-player games).

PDF Details DOI

TIME Conference 2017 Conference Paper

Timed-Automata-Based Verification of MITL over Signals

Thomas Brihaye
Gilles Geeraerts
Hsi-Ming Ho
Benjamin Monmege

It has been argued that the most suitable semantic model for real-time formalisms is the non-negative real line (signals), i. e. the continuous semantics, which naturally captures the continuous evolution of system states. Existing tools like UPPAAL are, however, based on omega-sequences with timestamps (timed words), i. e. the pointwise semantics. Furthermore, the support for logic formalisms is very limited in these tools. In this article, we amend these issues by a compositional translation from Metric Temporal Interval Logic (MITL) to signal automata. Combined with an emptiness-preserving encoding of signal automata into timed automata, we obtain a practical automata-based approach to MITL model-checking over signals. We implement the translation in our tool MightyL and report on case studies using LTSmin as the back-end.

Details

Highlights Conference 2016 Conference Abstract

Real-Time Synthesis is Hard!

Thomas Brihaye
Morgane Estiévenart
Gilles Geeraerts
Hsi-Ming Ho
Benjamin Monmege
Nathalie Sznajder

We study the reactive synthesis problem (RS) for specifications given in Metric Interval Temporal Logic (MITL). RS is known to be undecidable in a very general setting, but on infinite words only; and only the very restrictive BResRS subcase is known to be decidable (see D’Souza et al. and Bouyer et al.). During this talk, we precise the decidability border of MITL synthesis. We show RS is undecidable on finite words too, and present a landscape of restrictions (both on the logic and on the possible controllers) that are still undecidable. On the positive side, we revisit BResRS and introduce an efficient on-the-fly algorithm to solve it. This is joint work (submitted at FORMATS 2016) with Thomas Brihaye, Morgane Estiévenart, Gilles Geeraerts, Hsi-Ming Ho, and Nathalie Sznajder.

Details

Highlights Conference 2016 Conference Abstract

Simple Priced Timed Games are not That Simple

Thomas Brihaye
Gilles Geeraerts
Axel Haddad
Engel Lefaucheux
Benjamin Monmege

Article published in FSTTCS 2015. Priced timed games are two-player zero-sum games played on priced timed automata (whose locations and transitions are labeled by weights modeling the costs of spending time in a state and executing an action, respectively). The goals of the players are to minimise and maximise the cost to reach a target location, respectively. We consider priced timed games with one clock and arbitrary (positive and negative) weights and show that, for an important subclass of theirs (the so-called simple priced timed games), one can compute, in exponential time, the optimal values that the players can achieve, with their associated optimal strategies. As side results, we also show that one-clock priced timed games are determined and that we can use our result on simple priced timed games to solve the more general class of so-called reset-acyclic priced timed games (with arbitrary weights and one-clock).

Details

I&C Journal 2015 Journal Article

Simple strategies for Banach–Mazur games and sets of probability 1

Thomas Brihaye
Axel Haddad
Quentin Menet

In 2006, Varacca and Völzer proved that on finite graphs, ω-regular large sets coincide with ω-regular sets of probability 1, by using the existence of positional strategies in the related Banach–Mazur games. Motivated by this result, we try to understand relations between sets of probability 1 and various notions of simple strategies (including those introduced in a recent paper of Grädel and Leßenich). Then, we introduce a generalisation of the classical Banach–Mazur game and in particular, a probabilistic version whose goal is to characterise sets of probability 1 (as classical Banach–Mazur games characterise large sets). We obtain a determinacy result for these games, when the winning set is a countable intersection of open sets.

Details DOI

CSL Conference 2015 Conference Paper

Weak Subgame Perfect Equilibria and their Application to Quantitative Reachability

Thomas Brihaye
Véronique Bruyère
Noémie Meunier
Jean-François Raskin

We study n-player turn-based games played on a finite directed graph. For each play, the players have to pay a cost that they want to minimize. Instead of the well-known notion of Nash equilibrium (NE), we focus on the notion of subgame perfect equilibrium (SPE), a refinement of NE well-suited in the framework of games played on graphs. We also study natural variants of SPE, named weak (resp. very weak) SPE, where players who deviate cannot use the full class of strategies but only a subclass with a finite number of (resp. a unique) deviation step(s). Our results are threefold. Firstly, we characterize in the form of a Folk theorem the set of all plays that are the outcome of a weak SPE. Secondly, for the class of quantitative reachability games, we prove the existence of a finite-memory SPE and provide an algorithm for computing it (only existence was known with no information regarding the memory). Moreover, we show that the existence of a constrained SPE, i. e. an SPE such that each player pays a cost less than a given constant, can be decided. The proofs rely on our Folk theorem for weak SPEs (which coincide with SPEs in the case of quantitative reachability games) and on the decidability of MSO logic on infinite words. Finally with similar techniques, we provide a second general class of games for which the existence of a (constrained) weak SPE is decidable.

Details

Highlights Conference 2013 Conference Abstract

On the decidability of priced timed games

Thomas Brihaye
Gilles Geeraerts
S. Krishna
Lakshmi Manasa
Ashutosh Trivedi

Two-player zero-sum games on finite automata are a classical metaphor for controller synthesis. An extension of this model to time-critical systems are two-player games on priced timed automata. For those games, the optimal reachability synthesis problem asks to compute a strategy (for one of the players) that guarantees to reach a given target with a total cost satisfying some optimality constraint. While, some versions of this problem have already been showed undecidable, we propose to complete the global picture by studying other variants (such as the timed-bounded version).

PDF Details

Highlights Conference 2013 Conference Abstract

Simple strategies for Banach-Mazur games and fairly correct systems

Thomas Brihaye
Quentin Menet

In 2006, Varacca and Voelzer proved that on finite graphs, omega-regular large sets coincide with omega-regular sets of probability 1, by using the existence of positional strategies in the related Banach-Mazur games. Motivated by this result, we try to understand relations between sets of probability~1 and various notions of simple strategy (including those introduced in a recent paper of Graedel and Lessenich). Then, we introduce a generalisation of the classical Banach-Mazur game and in particular, a probabilistic version whose goal is to characterise sets of probability~1 (as classical Banach-Mazur games characterise large sets). We obtain a determinacy result for these games, when the winning set is a countable intersection of open sets.

PDF Details

GandALF Workshop 2013 Workshop Paper

Simple strategies for Banach-Mazur games and fairly correct systems

Thomas Brihaye
Quentin Menet

In 2006, Varacca and Völzer proved that on finite graphs, omega-regular large sets coincide with omega-regular sets of probability 1, by using the existence of positional strategies in the related Banach-Mazur games. Motivated by this result, we try to understand relations between sets of probability 1 and various notions of simple strategies (including those introduced in a recent paper of Grädel and Lessenich). Then, we introduce a generalisation of the classical Banach-Mazur game and in particular, a probabilistic version whose goal is to characterise sets of probability 1 (as classical Banach-Mazur games characterise large sets). We obtain a determinacy result for these games, when the winning set is a countable intersection of open sets.

PDF Details DOI

TIME Conference 2008 Conference Paper

Good Friends are Hard to Find!

Thomas Brihaye
Nicolas Markey
Mohamed Ghannem
Lionel Rieg

We focus on the problem of finding (the size of) a minimal winning coalition in a multi-player game. We prove that deciding whether there is a winning coalition of size at most k is HP-complete, while deciding whether k is the optimal size is DP -complete. We also study different variants of our original problem: the function problem, where the aim is to effectively compute the coalition; more succinct encoding of the game; and richer families of winning objectives.

Details

I&C Journal 2006 Journal Article

On model-checking timed automata with stopwatch observers

Thomas Brihaye
Véronique Bruyère
Jean-François Raskin

In this paper, we study the model-checking problem for weighted timed automata and the weighted CTL logic; we also study the finiteness of bisimulations of weighted timed automata. Weighted timed automata are timed automata extended with costs on both edges and locations. When the costs act as stopwatches, we get stopwatch automata with the restriction that the stopwatches cannot be reset nor tested. The weighted CTL logic is an extension of TCTL that allows to reset and test the cost variables. Our main results are: (i) the undecidability of the proposed model-checking problem for discrete and dense time in general, (ii) its PSpace-Completeness in the discrete case, and its undecidability in the dense case, for a slight restriction of the weighted CTL Logic, (iii) the precise frontier between finite and infinite bisimulations in the dense case for the subclass of stopwatch automata.

Details DOI