Séminaire du 15 décembre 2017

Lieu

LACL, bâtiment P2-RdC, salle des thèses: comment y aller

Programme

14h00-15h00: Youssouf Oualhadj (LACL), " The Complexity of Concurrent Rational Synthesis

Abstract: 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. Given an instance of the rational synthesis problem, 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, Parity, Muller, Street, and Rabin are PSpace-hard and in ExpTime.

15h00-15h30 : Nguyen Hoàng Gia (LIPN), " Efficient Parameter Synthesis Using Optimized State Exploration Strategies

Abstract: Parametric timed automata are a powerful formalism to reason about, model and verify real-time systems in which some constraints are unknown, or subject to uncertainty. Parameter synthesis using parametric timed automata is very sensitive to the state space explosion problem. To mitigate this problem, we propose two new exploration orders, i. e., the "ranking strategy" and the "priority based strategy", and compare them with existing strategies. We consider both complete parameter synthesis, and counterexample synthesis where the analysis stops as soon as some parameter valuations are found. Experimental results using IMITATOR show that our new strategies significantly outperform existing approaches, especially in the counterexample synthesis.

15h30-16h00: pause café

16h00-16h30: vie du groupe