2021
[BBF+21] Giovanni Bacci, Patricia Bouyer, Uli Fahrenberg, Kim Guldstrand Larsen, Nicolas Markey et Pierre-Alain Reynier. Optimal and Robust Controller Synthesis Using Energy Timed Automata with Uncertainty. Formal Aspects of Computing 33(1):3-25. Springer-Verlag, janvier 2021.
Résumé

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 et Nicolas Markey. Diagnosing timed automata using timed markings. International Journal on Software Tools for Technology Transfer 23(2):229-253. Springer-Verlag, avril 2021.
Résumé

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.},
}
[AZZ+21] Jie An, Bohua Zhan, Naijun Zhan et Miaomiao Zhang. Learning nondeterministic real-time automata. ACM Transactions on Embedded Computing Systems 20(5s):99:1-99:26. ACM Press, octobre 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},
}
[BFF+21] Raphaël Berthon, Nathanaël Fijalkow, Emmanuel Filiot, Shibashis Guha, Bastien Maubert, Aniello Murano, Laureline Pinault, Sophie Pinchinat, Sasha Rubin et Olivier Serre. Alternating Tree Automata with Qualitative Semantics. ACM Transactions on Computational Logic 22(1):7:1-7:24. ACM Press, janvier 2021.
@article{tocl22(1)-BFFGMMPPRS,
  author =              {Berthon, Rapha{\"e}l and Fijalkow, Nathana{\"e}l and
                         Filiot, Emmanuel and Guha, Shibashis and Maubert,
                         Bastien and Murano, Aniello and Pinault, Laureline
                         and Pinchinat, Sophie and Rubin, Sasha and Serre,
                         Olivier},
  title =               {Alternating Tree Automata with Qualitative
                         Semantics},
  publisher =           {ACM Press},
  journal =             {ACM Transactions on Computational Logic},
  volume =              {22},
  number =              {1},
  pages =               {7:1-7:24},
  year =                {2021},
  month =               jan,
  doi =                 {10.1145/3431860},
}
[BL21] Udi Boker et Karoliina Lehtinen. History Determinism vs. Good for Gameness in Quantitative Automata. In FSTTCS'21, Leibniz International Proceedings in Informatics 213, pages 38:1-38:20. Leibniz-Zentrum für Informatik, décembre 2021.
@inproceedings{fsttcs2021-BK,
  author =              {Boker, Udi and Lehtinen, Karoliina},
  title =               {History Determinism vs.~Good for Gameness in
                         Quantitative Automata},
  editor =              {Boja{\'n}czyk, Miko{\l}aj and Chekuri, Chandra},
  booktitle =           {{P}roceedings of the 41st {C}onference on
                         {F}oundations of {S}oftware {T}echnology and
                         {T}heoretical {C}omputer {S}cience ({FSTTCS}'21)},
  acronym =             {{FSTTCS}'21},
  publisher =           {Leibniz-Zentrum f{\"u}r Informatik},
  series =              {Leibniz International Proceedings in Informatics},
  volume =              {213},
  pages =               {38:1-38:20},
  year =                {2021},
  month =               dec,
  doi =                 {10.4230/LIPIcs.FSTTCS.2021.38},
}
[Lod21] Christof Löding. Automata on infinite trees. In Jean-Éric Pin (eds.), Handbook of automata theory. EMS Press, 2021.
@incollection{hat-ch8,
  author =              {L{\"o}ding, Christof},
  title =               {Automata on infinite trees},
  editor =              {Pin, Jean-{\'E}ric},
  booktitle =           {Handbook of automata theory},
  publisher =           {EMS~Press},
  volume =              {1},
  pages =               {265-302},
  chapter =             {8},
  year =                {2021},
  doi =                 {10.4171/AUTOMATA-1/8},
}
[MPS+21] Bastien Maubert, Sophie Pinchinat, François Schwarzentruber et Silvia Stranieri. Concurrent Games in Dynamic Epistemic Logic. In IJCAI'20, pages 1877-1883. IJCAI organization, janvier 2021.
@inproceedings{ijcai2020-MPSS,
  author =              {Maubert, Bastien and Pinchinat, Sophie and
                         Schwarzentruber, Fran{\c c}ois and Stranieri,
                         Silvia},
  title =               {Concurrent Games in Dynamic Epistemic Logic},
  editor =              {Bessiere, Christian},
  booktitle =           {{P}roceedings of the 29th {I}nternational {J}oint
                         {C}onference on {A}rtificial {I}ntelligence
                         ({IJCAI}'20)},
  acronym =             {{IJCAI}'20},
  publisher =           {IJCAI organization},
  pages =               {1877-1883},
  year =                {2021},
  month =               jan,
  doi =                 {10.24963/ijcai.2020/260},
}
[Pin21] Jean-Éric Pin. Handbook of automata theory. EMS Press, 2021.
@book{hat-pin-1,
  title =               {Handbook of automata theory},
  editor =              {Pin, Jean-{\'E}ric},
  booktitle =           {Handbook of automata theory},
  publisher =           {EMS~Press},
  volume =              {1},
  year =                {2021},
  doi =                 {10.4171/AUTOMATA-1},
}
[Sad21] Suman Sadhukhan. A Verification Viewpoint on Network Congestion Games. PhD thesis, Université Rennes 1, France, Décembre 2021.
@phdthesis{phd-sadhukhan,
  author =              {Sadhukhan, Suman},
  title =               {A Verification Viewpoint on Network Congestion
                         Games},
  year =                {2021},
  month =               dec,
  school =              {Universit{\'e} Rennes~1, France},
}
[SK21] Neda Saeedloei et Feliks Kluźniak. Minimization of the Number of Clocks for Timed Scenarios. In SBMF'21, Lecture Notes in Computer Science 13130, pages 122-139. Springer-Verlag, 2021.
@inproceedings{sbmf2021-SK,
  author =              {Saeedloei, Neda and Klu{\'z}niak, Feliks},
  title =               {Minimization of the Number of Clocks for Timed
                         Scenarios},
  editor =              {Campos, S{\'e}rgio Vale Aguiar and Minea, Marius},
  booktitle =           {{P}roceedings of the24th {B}razilian {S}ymposium on
                         {F}ormal {M}ethods ({SBMF}'21)},
  acronym =             {{SBMF}'21},
  publisher =           {Springer-Verlag},
  series =              {Lecture Notes in Computer Science},
  volume =              {13130},
  pages =               {122-139},
  year =                {2021},
  confmonth =           {12},
  doi =                 {10.1007/978-3-030-92137-8_8},
}
Liste des auteurs