Jeudi 2 Juillet
Heure: 
12:30  13:30 
Lieu: 
Salle B107, bâtiment B, Université de Villetaneuse 
Résumé: 
Solving the quadratic shortest path problem 
Description: 
Borzou Rostami Finding the shortest path in a directed graph is one of the most important combinatorial optimization problems, having applications in a wide range of fields. In its basic version, however, the problem fails to represent situations in which the value of the objective function is determined not only by the choice of each single arc, but also by the combined presence of pairs of arcs in the solution. In this paper we model these situations as a Quadratic Shortest Path Problem, which calls for the minimization of a quadratic objective function subject to shortestpath constraints. We prove strong NPhardness of the problem and analyze polynomially solvable special cases, obtained by restricting the distance of arc pairs in the graph that appear jointly in a quadratic monomial of the objective function. Based on this special case and problem structure, we devise fast lower bounding procedures for the general problem and show computationally that they clearly outperform other approaches proposed in the literature in terms of their strength. 
Heure: 
14:30  15:30 
Lieu: 
Salle B107, bâtiment B, Université de Villetaneuse 
Résumé: 
Action synthesis for branching time logic: theory and applications 
Description: 
Micha? Knapik ActionRestricted Computation Tree Logic (ARCTL) is a simple extension of CTL, proposed by Pecheur and Raimondi, where the actions allowed along the considered runs can be explicitly indicated by path selectors. ARCTL allows to express properties such as "a safe state is unavoidable for every path built from Forward and Left actions", denoted by AF{Forward,Safe}safe. By replacing the concrete sets of actions with free variables we obtain a parametric version of the logic pmARCTL, where properties such as AF{X}safe are allowed, where X is a parameter. We introduce a fixedpoint theory that allows for the exhaustive synthesis of all the valuations of the variables which make the pmARTCL formulae hold in a given model. The theory has been implemented in an open source standalone tool and evaluated on scalable examples with promising results. 

