Optimal and robust controller synthesis using energy timed automata with uncertainty
- PDF / 895,628 Bytes
- 23 Pages / 595.276 x 790.866 pts Page_size
- 28 Downloads / 205 Views
Formal Aspects of Computing
Optimal and robust controller synthesis1 using energy timed automata with uncertainty Giovanni Bacci 1 , Patricia Bouyer2 , Uli Fahrenberg3 , Kim G. Larsen1 , Nicolas Markey4 , Pierre-Alain Reynier5 1 Department 2 LSV, CNRS
¨ Vej 300, 9220 Aalborg Øst, Denmark, of Computer Science, Aalborg University, Selma Lagerlofs & ENS Cachan, Universit´e Paris-Saclay, Cachan, France 3 Ecole ´ Polytechnique, Palaiseau, France 4 IRISA, CNRS & INRIA, Univ. Rennes, Rennes, France 5 CNRS, LIS, Aix Marseille Univ., Universit´ e de Toulon, Marseille, France
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. Keywords: Energy timed automata; Controller synthesis; Quantifier elimination
1. Introduction Design of controllers for embedded systems is a difficult engineering task. Controllers must ensure a variety of safety properties as well as optimality with respect to given performance properties. Also, for several systems, e.g. [BGH+ 16, vBHLO17, PHM14], the properties involve non-functional aspects such as time and energy. We provide a novel framework for automatic synthesis of safe and optimal controllers for resource-aware systems based on energy timed automata. Synthesis of controllers is obtained by solving time- and energyconstrained infinite run problems. Energy timed automata [BFL+ 08] extend timed automata [AD94] with a continuous energy variable that evolves with varying rates and discrete updates during the behaviour of the model. Addressing an open problem from [BFL+ 08], we prove decidability of the infinite run problem in settings where rates and updates may be both positive and negative and possibly subject to uncertainty.
1
Work supported by ERC projects Lasso and EQualIS and by French ANR project TickTac.
Correspondence to: Giovanni Bacci, e-mail: [email protected]
G. Bacci et al.
l/s Accumulator Vmax
Vmin
Machine
(a)
machine rate
2.2 l/s
Pump
3.0 2.8 2.6 2.4 2.2 2.0 1.8 1.6 1.4 1.2 1.0 0.8 0.6 0.4 0.2 0.0
0
2
4
System Components
6
(b)
8
10
time
12
14
16
18
20
s
Cycle of the Machine
Fig. 1. Overview of the HYDAC system
Additionally, the accumulated energy may be subject to lower and upper bounds reflecting constraints on capacity. Also we consider the optimization problems of identifying minima
Data Loading...
