Invited Speakers

Saddek Bensalem (Université Grenoble Alpes)

Saddek Bensalem

Title Rigorous System Design: The BIP Framework

Abstract Rigorous system design requires the use of a single powerful component framework allowing the representation of the designed system at different levels of detail, from application software to its implementation. This is essential for ensuring the overall coherency and correctness. This talk introduces a rigorous design flow based on the BIP (Behavior, Interaction, Priority) component framework. This design flow relies on several, tool-supported, source-to-source transformations allowing to progressively and correctly transform high level application software towards efficient implementations for specific platforms.

Véronique Bruyère (University of Mons)

Véronique Bruyère

Title On the Synthesis of Equilibria in Graph Games

Abstract In this invited talk, we focus on games played on graphs by several players who aim at satisfying their objective. We survey and discuss several solution concepts useful for the synthesis of systems, the most famous one being the notion of Nash equilibrium. We present several results about their existence (possibly constrained by some conditions on the payoffs), the objectives of the players being qualitative or quantitative. We also provide some illustrative examples as well as intuitions on the proofs.

Kim G. Larsen (Aalborg University)

Kim G. Larsen

Title Energy Timed Automata and Games

Abstract The first part of the talk will provide an overview of the results obtained over the last 10 years when considering Timed Automata and Timed Games extended with continuous variables (cost) that may evolve with different (positive or negative) weights with particular interest in infinite energy-bounded runs/strategies. In the second part we review recent results obtained for a subclass called Segmented Energy Timed Games, where we have decidability, thus allowing for the automatic synthesis of robust and optimal energy-aware controllers. We prove decidability of the energy-constrained infinite run problem in settings with both certainty and uncertainty of the energy-rates. We also consider the optimization problem of identifying the minimal upper bound that will permit existence of infinite energy constrained runs. Our algorithms are based on quantifier elimination for linear real arithmetic. Using Mathematica and Mjollnir, we illustrate our framework through a real industrial example of a hydraulic oil pump. Compared with previous approaches our method is completely automated and provides significantly improved results.

Holger Hermanns (Saarland University)

Holger Hermanns

Title Battery-Aware Scheduling in Low Orbit - The GomX-3 Case

Abstract For a satellite in orbit all resources are sparse and the most critical resource of all is power. It is therefore crucial to have detailed knowledge on how much power is available for an energy harvesting satellite in orbit at every time – especially when in eclipse, where it draws its power from onboard batteries. This paper addresses this problem by a two-step procedure to perform task scheduling for low-earth-orbit (LEO) satellites exploiting formal methods. It combines cost-optimal reachability analyses of priced timed automata networks with a realistic kinetic battery model capable of capturing capacity limits as well as stochastic fluctuations. The procedure has been used for the automatic and resource-optimal day-ahead scheduling of GomX-3, a power-hungry nanosatellite currently orbiting the earth. We explain how this approach has overcome existing problems, has led to improved designs, and has provided new insights.


  • Sep 11, 2018: Proceedings published
  • Aug 21, 2018: Program is online
  • Aug 16, 2018: Room block at Hotel Madeleine extended until August 22
  • Aug 1, 2018: Registration opened
  • Aug 1, 2018: Accepted Papers and Local Information added
  • Jun 14, 2018: Deadline extended
  • Apr 24, 2018: Special Issue announced
  • Feb 18, 2018: Invited speakers added
  • Jan 19, 2018: PC added
  • Jan 18, 2018: We are online

Important Dates

All dates are Anywhere on Earth.

  • Abstract submission:
    June 13th 20th, 2018
  • Paper submission:
    June 15th 22nd, 2018
  • Notification:
    August 1st, 2018
  • Camera-ready:
    August 17th, 2018
  • Conference:
    September 26th - 28th, 2018