Séminaires
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.