Léonard Brice, Jean-François Raskin and Marie Van Den Bogaard
Subgame-perfect Equilibria in Mean-payoff Games
Abstract: 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 are supported by SPEs are exactly those that are consistent with the least fixed point of the negotiation function. Finally, we show that the negotiation function is piecewise linear, and can be analyzed using the linear algebraic tool box. As a corollary, we prove the decidability of the SPE constrained existence problem, whose status was left open in the literature.
Cláudio Belo Lourenço, Denis Cousineau, Florian Faissole, Claude Marché, David Mentré and Hiroaki Inoue
Automated Verification of Temporal Properties of Ladder Programs
This paper is an excellent example of the results that can be achieved in a joint academia-industry collaboration through the use of formal methods. This is also reflected in the following sentences from the reviewers:
- "The paper is very relevant for FMICS: It shows a good example of how formal methods can be applied for industrial applications."
- "This work is definitely of industrial interest for both legacy Ladder programs and programs to be developed."
Eugène Asarin, Thomas Ferrère, Dejan Ničković and Doǧan Ulus
On the complexity of Timed Pattern Matching
Grzegorz Kielanski and Benny Van Houdt
Performance analysis of work stealing strategies in large scale multi-threaded computing
Additionally, a best RAE paper award was given:
Carina Pilch, Stefan Schupp and Anne Remke
Optimizing reachability probabilities for a restricted class of Stochastic Hybrid Automata via Flowpipe-Construction