2021 | |
---|---|

[BBF+21] | Giovanni Bacci,
Patricia Bouyer,
Uli Fahrenberg,
Kim Guldstrand Larsen,
Nicolas Markey, and
Pierre-Alain Reynier.
Optimal and Robust Controller Synthesis Using Energy
Timed Automata with Uncertainty.
Formal Aspects of Computing 33(1):3-25. Springer-Verlag, January 2021.
- 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.}, } |

[BHJ+21] | Patricia Bouyer,
Léo Henry,
Samy Jaziri,
Thierry Jéron, and
Nicolas Markey.
Diagnosing timed automata using timed markings.
International Journal on Software Tools for
Technology Transfer 23(2):229-253. Springer-Verlag, April 2021.
- Abstract
We consider the problems of efficiently diagnosing (and predicting) what did (and will) happen after a given sequence of observations of the execution of a partially-observable one-clock timed automaton. This is made difficult by the facts that timed automata are infinite-state systems, and that they can in general not be determinized. We introduce timed markings as a formalism to keep track of the evolution of the set of reachable configurations over time. We show how timed markings can be used to efficiently represent the closure under silent transitions of such automata. We report on our implementation of this approach compared to the approach of [Tripakis, Fault diagnosis for timed automata, 2002], and provide some insight to a generalization of our approach to n-clock timed automata.
@article{sttt23(2)-BHJJM, author = {Bouyer, Patricia and Henry, L{\'e}o and Jaziri, Samy and J{\'e}ron, Thierry and Markey, Nicolas}, title = {Diagnosing timed automata using timed markings}, publisher = {Springer-Verlag}, journal = {International Journal on Software Tools for Technology Transfer}, volume = {23}, number = {2}, pages = {229-253}, year = {2021}, month = apr, doi = {10.1007/s10009-021-00606-2}, abstract = {We~consider the problems of efficiently diagnosing (and~predicting) what did (and~will) happen after a given sequence of observations of the execution of a partially-observable one-clock timed automaton. This is made difficult by the facts that timed automata are infinite-state systems, and that they can in general not be determinized. \par We~introduce timed markings as a formalism to keep track of the evolution of the set of reachable configurations over time. We show how timed markings can be used to efficiently represent the closure under silent transitions of such automata. We report on our implementation of this approach compared to the approach of [Tripakis, Fault diagnosis for timed automata,~2002], and provide some insight to a generalization of our approach to {{\(n\)}}-clock timed automata.}, } |

[HMR21] | Loïc Hélouët,
Nicolas Markey, and
Ritam Raha.
Reachability games with relaxed energy constraints.
Information and Computation.
Elsevier, 2021. To appear.
- Abstract
We study games with reachability objectives under energy constraints. We first prove that under strict energy constraints (either only lower-bound constraint or interval constraint), those games are LOGSPACE-equivalent to energy games with the same energy constraints but without reachability objective (i.e., for infinite runs). We then consider two relaxations of the upper-bound constraints (while keeping the lower-bound constraint strict): in the first one, called weak upper bound, the upper bound is absorbing, i.e., when the upper bound is reached, the extra energy is not stored; in the second one, we allow for temporary violations of the upper bound, imposing limits on the number or on the amount of violations. We prove that when considering weak upper bound, reachability objectives require memory, but can still be solved in polynomial-time for one-player arenas; we prove that they are in NP in the two-player setting. Allowing for bounded violations makes the problem PSPACE-complete for one-player arenas and EXPTIME-complete for two players. We then address the problem of existence of bounds for a given arena. We show that with reachability objectives, existence can be a simpler problem than the game itself, and conversely that with infinite games, existence can be harder.
@article{icomp2021-HMR, author = {H{\'e}lou{\"e}t, Lo{\"\i}c and Markey, Nicolas and Raha, Ritam}, title = {Reachability games with relaxed energy constraints}, publisher = {Elsevier}, journal = {Information and Computation}, year = {2021}, doi = {10.1016/j.ic.2021.104806}, note = {To~appear}, abstract = {We study games with reachability objectives under energy constraints. We first prove that under strict energy constraints (either only lower-bound constraint or interval constraint), those games are LOGSPACE-equivalent to energy games with the same energy constraints but without reachability objective (i.e., for infinite runs). We then consider two relaxations of the upper-bound constraints (while keeping the lower-bound constraint strict): in the first one, called weak upper bound, the upper bound is absorbing, i.e., when the upper bound is reached, the extra energy is not stored; in the second one, we allow for temporary violations of the upper bound, imposing limits on the number or on the amount of violations. \par We prove that when considering weak upper bound, reachability objectives require memory, but can still be solved in polynomial-time for one-player arenas; we prove that they are in NP in the two-player setting. Allowing for bounded violations makes the problem PSPACE-complete for one-player arenas and EXPTIME-complete for two players. We then address the problem of existence of bounds for a given arena. We show that with reachability objectives, existence can be a simpler problem than the game itself, and conversely that with infinite games, existence can be harder.}, } |

[AZZ+21] | Jie An,
Bohua Zhan,
Naijun Zhan, and
Miaomiao Zhang.
Learning nondeterministic real-time automata.
ACM Transactions on Embedded Computing Systems 20(5s):99:1-99:26. ACM Press, October 2021.
@article{tecs20(5s)-AZZZ, author = {An, Jie and Zhan, Bohua and Zhan, Naijun and Zhang, Miaomiao}, title = {Learning nondeterministic real-time automata}, publisher = {ACM Press}, journal = {ACM Transactions on Embedded Computing Systems}, volume = {20}, number = {5s}, pages = {99:1-99:26}, year = {2021}, month = oct, doi = {10.1145/3477030}, } |

- Patricia Bouyer
- Giovanni Bacci
- Uli Fahrenberg
- Kim Guldstrand Larsen
- Pierre-Alain Reynier
- Léo Henry
- Samy Jaziri
- Thierry Jéron
- Loïc Hélouët
- Ritam Raha
- Jie An
- Bohua Zhan
- Naijun Zhan
- Miaomiao Zhang