Search

• < Previous
• 1
• Next >

---

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;]

---

On the Sets of Real Numbers Recognized by Finite Automata in Multiple Bases

Bernard Boigelot ; Julien Brusten ; Veronique Bruyere.

This article studies the expressive power of finite automata recognizing sets of real numbers encoded in positional notation. We consider Muller automata as well as the restricted class of weak deterministic automata, used as symbolic set representations in actual applications. In previous work, it&nbsp;[&hellip;]

---

On (Subgame Perfect) Secure Equilibrium in Quantitative Reachability Games

Thomas Brihaye ; Véronique Bruyère ; Julie De Pril ; Hugo Gimbert.

We study turn-based quantitative multiplayer non zero-sum games played on finite graphs with reachability objectives. In such games, each player aims at reaching his own goal set of states as soon as possible. A previous work on this model showed that Nash equilibria (resp. secure equilibria) are&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;]

---