Search

• < Previous
• 1
• Next >

---

Antichains for the Automata-Based Approach to Model-Checking

Laurent Doyen ; Jean-Francois Raskin.

We propose and evaluate antichain algorithms to solve the universality and language inclusion problems for nondeterministic Buechi automata, and the emptiness problem for alternating Buechi automata. To obtain those algorithms, we establish the existence of simulation pre-orders that can be&nbsp;[&hellip;]

---

Algorithms for Omega-Regular Games with Imperfect Information

Krishnendu Chatterjee ; Laurent Doyen ; Thomas A. Henzinger ; Jean-Francois Raskin.

We study observation-based strategies for two-player turn-based games on graphs with omega-regular objectives. An observation-based strategy relies on imperfect information about the history of a play, namely, on the past sequence of observations. Such games occur in the synthesis of a controller&nbsp;[&hellip;]

---

Real-Time Model-Checking: Parameters everywhere

Veronique Bruyere ; Jean-Francois Raskin.

In this paper, we study the model-checking and parameter synthesis problems of the logic TCTL over discrete-timed automata where parameters are allowed both in the model (timed automaton) and in the property (temporal formula). Our results are as follows. On the negative side, we show that the&nbsp;[&hellip;]

---

The Complexity of Subgame Perfect Equilibria in Quantitative Reachability Games

Thomas Brihaye ; Véronique Bruyère ; Aline Goeminne ; Jean-François Raskin ; Marie van den Bogaard.

We study multiplayer quantitative reachability games played on a finite directed graph, where the objective of each player is to reach his target set of vertices as quickly as possible. Instead of the well-known notion of Nash equilibrium (NE), we focus on the notion of subgame perfect equilibrium&nbsp;[&hellip;]

---

Subgame-perfect Equilibria in Mean-payoff Games (journal version)

Léonard Brice ; Marie van den Bogaard ; Jean-François Raskin.

In this paper, we provide an effective characterization of all the subgame-perfect equilibria in infinite duration games played on finite graphs with mean-payoff objectives. To this end, we introduce the notion of requirement, and the notion of negotiation function. We establish that the plays that&nbsp;[&hellip;]

---