Séminaires
Séminaire du 2 juin 2017
Lieu
LIPN, CNRS UMR 7030, Université Paris 13, Institut Galilée, salle B107.
Programme
14h00-15h00: Jaco van de Pol (Univ. Twente), "Energy-optimization for Dataflow Applications using Timed Automata"
Joint work with: Waheed Ahmad, Marielle Stoelinga
Abstract : 
Streaming applications on mobile devices pose challenging performance and energy constraints. An energy-aware solution would run on a minimal energy budget, without violating quality constraints. In order to program such systems on heterogeneous hardware, powerful models and tools are essential. We have experimented with synchronous dataflow models of an application's functionality. The available processors with their performance and energy saving capabilities are described in a hardware platform model, including dynamic power management and voltage-frequency scaling. Using model transformation technology, both models are combined and transformed to extended Timed Automata. Powerful optimisation and synthesis algorithms, provided by the UPPAAL tool suite, can then be used to compute energy-optimal schedules that satisfy all performance criteria.
15h00-16h00 : Wojciech Penczek(Univ. Warsaw), "Timed ATL: Forget Memory, Just Count"
Joint work with: Étienne André, Laure Petrucci, Wojciech Jamroga, Michal Knapik
Abstract : We investigate Timed Alternating-Time Temporal Logic (TATL), a discrete-time extension of ATL. A new semantics based on counting the number of visits in locations in the history is introduced in addition to timed memoryful and memoryless ones.
We show that all the defined semantics are equivalent for TATL_{≤,≥}, i.e., when = is not allowed in the formulae. We provide a strategy analysis for TATL_{≤,≥} revealing that it suffices to consider
only two actions per location to verify any TATL_{≤,≥} formula. As we show, this does not extend to full TATL. The above results allow for building a hierarchy of strategies comparing the expressive power of the logics against ATL.