Nicolas Markey

Abstract

In this paper, we propose a novel framework for the synthesis of robust and optimal energy-aware controllers. The framework is based on energy timed automata, allowing for easy expression of timing-constraints and variable energy-rates. 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 energy-constrained infinite 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 improved results.

@article{fac2020-BBFLMR,
  author =              {Bacci, Giovanni and Bouyer, Patricia and Fahrenberg,
                         Uli and Larsen, Kim Guldstrand and Markey, Nicolas
                         and Reynier, Pierre-Alain},
  title =               {Optimal and Robust Controller Synthesis Using Energy
                         Timed Automata with Uncertainty},
  publisher =           {Springer-Verlag},
  journal =             {Formal Aspects of Computing},
  volume =              {33},
  number =              {1},
  pages =               {3-25},
  year =                {2021},
  month =               jan,
  doi =                 {10.1007/s00165-020-00521-4},
  abstract =            {In~this paper, we~propose a novel framework for the
                         synthesis of robust and optimal energy-aware
                         controllers. The~framework is based on energy timed
                         automata, allowing for easy expression of
                         timing-constraints and variable energy-rates.
                         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
                         energy-constrained infinite 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 improved results.},
}