2017
[BMP+17] Patricia Bouyer, Nicolas Markey, Nicolas Perrin et Philipp Schlehuber-Caissier. Timed automata abstraction of switched dynamical systems using control funnels. Real-Time Systems 53(3):327-353. Kluwer Academic, mai 2017.
Résumé

The development of formal methods for control design is an important challenge with potential applications in a wide range of safety-critical cyber-physical systems. Focusing on switched dynamical systems, we propose a new abstraction, based on time-varying regions of invariance (control funnels), that models behaviors of systems as timed automata. The main advantage of this method is that it allows for the automated verification and reactive controller synthesis without discretizing the evolution of the state of the system. Efficient and analytic constructions are possible in the case of linear dynamics whereas bounding funnels with conjectured properties based on numerical simulations can be used for general nonlinear dynamics. We demonstrate the potential of our approach with three examples.

@article{rts53(3)-BMPS,
  author =              {Bouyer, Patricia and Markey, Nicolas and Perrin,
                         Nicolas and Schlehuber{-}Caissier, Philipp},
  title =               {Timed automata abstraction of switched dynamical
                         systems using control funnels},
  publisher =           {Kluwer Academic},
  journal =             {Real-Time Systems},
  volume =              {53},
  number =              {3},
  pages =               {327-353},
  year =                {2017},
  month =               may,
  doi =                 {10.1007/s11241-016-9262-3},
  abstract =            {The development of formal methods for control design
                         is an important challenge with potential
                         applications in a wide range of safety-critical
                         cyber-physical systems. Focusing on switched
                         dynamical systems, we propose a new abstraction,
                         based on time-varying regions of invariance (control
                         funnels), that models behaviors of systems as timed
                         automata. The~main advantage of this method is that
                         it allows for the automated verification and
                         reactive controller synthesis without discretizing
                         the evolution of the state of the system. Efficient
                         and analytic constructions are possible in the case
                         of linear dynamics whereas bounding funnels with
                         conjectured properties based on numerical
                         simulations can be used for general nonlinear
                         dynamics. We~demonstrate the potential of our
                         approach with three examples.},
}
[BMV17] Patricia Bouyer, Nicolas Markey et Steen Vester. Nash Equilibria in Symmetric Graph Games with Partial Observation. Information and Computation 254(2):238-258. Elsevier, juin 2017.
Résumé

We investigate a model for representing large multiplayer games, which satisfy strong symmetry properties. This model is made of multiple copies of an arena; each player plays in his own arena, and can partially observe what the other players do. Therefore, this game has partial information and symmetry constraints, which make the computation of Nash equilibria difficult. We show several undecidability results, and for bounded-memory strategies, we precisely characterize the complexity of computing pure Nash equilibria (for qualitative objectives) in this game model.

@article{icomp254()-BMV,
  author =              {Bouyer, Patricia and Markey, Nicolas and Vester,
                         Steen},
  title =               {{N}ash Equilibria in Symmetric Graph Games with
                         Partial Observation},
  publisher =           {Elsevier},
  journal =             {Information and Computation},
  volume =              {254},
  number =              {2},
  pages =               {238-258},
  year =                {2017},
  month =               jun,
  doi =                 {10.1016/j.ic.2016.10.010},
  abstract =            {We investigate a model for representing large
                         multiplayer games, which satisfy strong symmetry
                         properties. This model is made of multiple copies of
                         an arena; each player plays in his own arena, and
                         can partially observe what the other players do.
                         Therefore, this game has partial information and
                         symmetry constraints, which make the computation of
                         Nash equilibria difficult. We show several
                         undecidability results, and for bounded-memory
                         strategies, we precisely characterize the complexity
                         of computing pure Nash equilibria (for qualitative
                         objectives) in this game model.},
}
[BHM+17] Patricia Bouyer, Piotr Hofman, Nicolas Markey, Mickael Randour et Martin Zimmermann. Bounding Average-energy Games. In FoSSaCS'17, Lecture Notes in Computer Science 10203, pages 179-195. Springer-Verlag, avril 2017.
Résumé

We consider average-energy games, where the goal is to minimize the long-run average of the accumulated energy. Decidability of average-energy games with a lower-bound constraint on the energy level (but no upper bound) is an open problem; in particular, there is no known upper bound on the memory that is required for winning strategies.

By reducing average-energy games with lower-bounded energy to infinite-state mean-payoff games and analyzing the frequency of low-energy configurations, we show an almost tight doubly-exponential upper bound on the necessary memory, and that the winner of average-energy games with lower-bounded energy can be determined in doubly-exponential time. We also prove EXPSPACE-hardness of this problem.

Finally, we consider multi-dimensional extensions of all types of average-energy games: without bounds, with only a lower bound, and with both a lower and an upper bound on the energy. We show that the fully-bounded version is the only case to remain decidable in multiple dimensions.

@inproceedings{fossacs2017-BHMRZ,
  author =              {Bouyer, Patricia and Hofman, Piotr and Markey,
                         Nicolas and Randour, Mickael and Zimmermann, Martin},
  title =               {Bounding Average-energy Games},
  editor =              {Esparza, Javier and Murawski, Andrzej},
  booktitle =           {{P}roceedings of the 20th {I}nternational
                         {C}onference on {F}oundations of {S}oftware
                         {S}cience and {C}omputation {S}tructure
                         ({FoSSaCS}'17)},
  acronym =             {{FoSSaCS}'17},
  publisher =           {Springer-Verlag},
  series =              {Lecture Notes in Computer Science},
  volume =              {10203},
  pages =               {179-195},
  year =                {2017},
  month =               apr,
  doi =                 {10.1007/978-3-662-54458-7_11},
  abstract =            {We~consider average-energy games, where the goal is
                         to minimize the long-run average of the accumulated
                         energy. Decidability of average-energy games with a
                         lower-bound constraint on the energy level (but~no
                         upper bound) is an open problem; in~particular,
                         there is no known upper bound on the memory that is
                         required for winning strategies.\par By~reducing
                         average-energy games with lower-bounded energy to
                         infinite-state mean-payoff games and analyzing the
                         frequency of low-energy configurations, we~show an
                         almost tight doubly-exponential upper bound on the
                         necessary memory, and that the winner of
                         average-energy games with lower-bounded energy can
                         be determined in doubly-exponential time. We~also
                         prove EXPSPACE-hardness of this problem.\par
                         Finally, we~consider multi-dimensional extensions of
                         all types of average-energy games: without bounds,
                         with only a lower bound, and with both a lower and
                         an upper bound on the energy. We show that the
                         fully-bounded version is the only case to remain
                         decidable in multiple dimensions.},
}
[BJM17] Patricia Bouyer, Samy Jaziri et Nicolas Markey. On the determinization of timed systems. In FORMATS'17, Lecture Notes in Computer Science 10419, pages 25-41. Springer-Verlag, septembre 2017.
Résumé

We introduce a new formalism called automata over a timed domain which provides an adequate framework for the determinization of timed systems. In this formalism, determinization w.r.t. timed language is always possible at the cost of changing the timed domain. We give a condition for determinizability of automata over a timed domain without changing the timed domain, which allows us to recover several known determinizable classes of timed systems, such as strongly-non-zeno timed automata, integer-reset timed automata, perturbed timed automata, etc. Moreover in the case of timed automata this condition encompasses most determinizability conditions from the literature.

@inproceedings{formats2017-BJM,
  author =              {Bouyer, Patricia and Jaziri, Samy and Markey,
                         Nicolas},
  title =               {On the determinization of timed systems},
  editor =              {Abate, Alessandro and Geeraerts, Gilles},
  booktitle =           {{P}roceedings of the 15th {I}nternational
                         {C}onferences on {F}ormal {M}odelling and {A}nalysis
                         of {T}imed {S}ystems ({FORMATS}'17)},
  acronym =             {{FORMATS}'17},
  publisher =           {Springer-Verlag},
  series =              {Lecture Notes in Computer Science},
  volume =              {10419},
  pages =               {25-41},
  year =                {2017},
  month =               sep,
  doi =                 {10.1007/978-3-319-65765-3_2},
  abstract =            {We introduce a new formalism called \emph{automata
                         over a timed domain} which provides an adequate
                         framework for the determinization of timed systems.
                         In~this formalism, determinization w.r.t. timed
                         language is always possible at the cost of changing
                         the timed domain. We~give a condition for
                         determinizability of automata over a timed domain
                         without changing the timed domain, which allows us
                         to recover several known determinizable classes of
                         timed systems, such as strongly-non-zeno timed
                         automata, integer-reset timed automata, perturbed
                         timed automata, etc. Moreover in the case of timed
                         automata this condition encompasses most
                         determinizability conditions from the literature.},
}
[Mar17] Nicolas Markey. Temporal logics for multi-agent systems (invited talk). In MFCS'17, Leibniz International Proceedings in Informatics 84, pages 84:1-84:3. Leibniz-Zentrum für Informatik, août 2017. 
@inproceedings{mfcs2017-Mar,
  author =              {Markey, Nicolas},
  title =               {Temporal logics for multi-agent systems
                         (invited~talk)},
  editor =              {Larsen, Kim Guldstrand and Bodlaender, Hans L. and
                         Raskin, Jean-Fran{\c c}ois},
  booktitle =           {{P}roceedings of the 42nd {I}nternational
                         {S}ymposium on {M}athematical {F}oundations of
                         {C}omputer {S}cience ({MFCS}'17)},
  acronym =             {{MFCS}'17},
  publisher =           {Leibniz-Zentrum f{\"u}r Informatik},
  series =              {Leibniz International Proceedings in Informatics},
  volume =              {84},
  pages =               {84:1-84:3},
  year =                {2017},
  month =               aug,
  doi =                 {10.4230/LIPIcs.MFCS.2017.84},
}
[BLM+17] Patricia Bouyer, François Laroussinie, Nicolas Markey, Joël Ouaknine et James Worrell. Timed temporal logics. In Luca Aceto, Giorgio Bacci, Giovanni Bacci, Anna Ingólfsdóttir, Axel Legay et Radu Mardare (eds.), Models, Algorithms, Logics and Tools: Essays Dedicated to Kim Guldstrand Larsen on the Occasion of His 60th Birthday, Lecture Notes in Computer Science 10460, pages 211-230. Springer-Verlag, août 2017.
Résumé

Since the early 1990's, classical temporal logics have been extended with timing constraints. While temporal logics only express contraints on the order of events, their timed extensions can add quantitative constraints on delays between those events. We survey expressiveness and algorithmic results on those logics, and discuss semantic choices that may look unimportant but do have an impact on the questions we consider.

@incollection{kimfest2017-BLMOW,
  author =              {Bouyer, Patricia and Laroussinie, Fran{\c c}ois and
                         Markey, Nicolas and Ouaknine, Jo{\"e}l and Worrell,
                         James},
  title =               {Timed temporal logics},
  editor =              {Aceto, Luca and Bacci, Giorgio and Bacci, Giovanni
                         and Ing{\'o}lfsd{\'o}ttir, Anna and Legay, Axel and
                         Mardare, Radu},
  booktitle =           {Models, Algorithms, Logics and Tools: Essays
                         Dedicated to Kim Guldstrand Larsen on the Occasion
                         of His 60th Birthday},
  publisher =           {Springer-Verlag},
  series =              {Lecture Notes in Computer Science},
  volume =              {10460},
  pages =               {211-230},
  year =                {2017},
  month =               aug,
  doi =                 {10.1007/978-3-319-63121-9_11},
  abstract =            {Since the early 1990's, classical temporal logics
                         have been extended with timing constraints. While
                         temporal logics only express contraints on the order
                         of events, their timed extensions can add
                         quantitative constraints on delays between those
                         events. We survey expressiveness and algorithmic
                         results on those logics, and discuss semantic
                         choices that may look unimportant but do have an
                         impact on the questions we consider.},
}
[ABD+17] Ernst Althaus, Björn Beber, Werner Damm, Stefan Disch, Willem Hagemann, Astrid Rakow, Christoph Scholl, Uwe Waldmann et Boris Wirtz. Verification of linear hybrid systems with large discrete state spaces using counterexample-guided abstraction refinement. Science of Computer Programming 148:123-160. Elsevier, novembre 2017. 
@article{scp148()-ABDDHRSWW,
  author =              {Althaus, Ernst and Beber, Bj{\"o}rn and Damm, Werner
                         and Disch, Stefan and Hagemann, Willem and Rakow,
                         Astrid and Scholl, Christoph and Waldmann, Uwe and
                         Wirtz, Boris},
  title =               {Verification of linear hybrid systems with large
                         discrete state spaces using counterexample-guided
                         abstraction refinement},
  publisher =           {Elsevier},
  journal =             {Science of Computer Programming},
  volume =              {148},
  pages =               {123-160},
  year =                {2017},
  month =               nov,
  doi =                 {10.1016/j.scico.2017.04.010},
}
[AGK17] Guy Avni, Shibashis Guha et Orna Kupferman. Timed Network Games. In MFCS'17, Leibniz International Proceedings in Informatics 84, pages 37:1-37:16. Leibniz-Zentrum für Informatik, août 2017. 
@inproceedings{mfcs2017-AGK,
  author =              {Avni, Guy and Guha, Shibashis and Kupferman, Orna},
  title =               {Timed Network Games},
  editor =              {Larsen, Kim Guldstrand and Bodlaender, Hans L. and
                         Raskin, Jean-Fran{\c c}ois},
  booktitle =           {{P}roceedings of the 42nd {I}nternational
                         {S}ymposium on {M}athematical {F}oundations of
                         {C}omputer {S}cience ({MFCS}'17)},
  acronym =             {{MFCS}'17},
  publisher =           {Leibniz-Zentrum f{\"u}r Informatik},
  series =              {Leibniz International Proceedings in Informatics},
  volume =              {84},
  pages =               {37:1-37:16},
  year =                {2017},
  month =               aug,
  doi =                 {10.4230/LIPIcs.MFCS.2017.37},
}
[AGK+17] S. Akshay, Paul Gastin, Shankara Narayanan Krishna et Ilias Sarkar. Towards an Efficient Tree Automata Based Technique for Timed Systems. In CONCUR'17, Leibniz International Proceedings in Informatics 85, pages 39:1-39:15. Leibniz-Zentrum für Informatik, septembre 2017. 
@inproceedings{concur2017-AGKS,
  author =              {Akshay, S. and Gastin, Paul and Krishna, Shankara
                         Narayanan and Sarkar, Ilias},
  title =               {Towards an Efficient Tree Automata Based Technique
                         for Timed Systems},
  editor =              {Meyer, Roland and Nestmann, Uwe},
  booktitle =           {{P}roceedings of the 28th {I}nternational
                         {C}onference on {C}oncurrency {T}heory
                         ({CONCUR}'17)},
  acronym =             {{CONCUR}'17},
  publisher =           {Leibniz-Zentrum f{\"u}r Informatik},
  series =              {Leibniz International Proceedings in Informatics},
  volume =              {85},
  pages =               {39:1-39:15},
  year =                {2017},
  month =               sep,
  doi =                 {10.4230/LIPIcs.CONCUR.2017.39},
}
[AKR+17] Shaull Almagor, Orna Kupferman, Jan Oliver Ringert et Yaron Velner. Quantitative Assume Guarantee Synthesis. In CAV'17, Lecture Notes in Computer Science 10427, pages 353-374. Springer-Verlag, juillet 2017. 
@inproceedings{cav2017-AKRV,
  author =              {Almagor, Shaull and Kupferman, Orna and Ringert, Jan
                         Oliver and Velner, Yaron},
  title =               {Quantitative Assume Guarantee Synthesis},
  editor =              {Majumdar, Rupak and Kuncak, Viktor},
  booktitle =           {{P}roceedings of the 29th {I}nternational
                         {C}onference on {C}omputer {A}ided {V}erification
                         ({CAV}'17)},
  acronym =             {{CAV}'17},
  publisher =           {Springer-Verlag},
  series =              {Lecture Notes in Computer Science},
  volume =              {10427},
  pages =               {353-374},
  year =                {2017},
  month =               jul,
  doi =                 {10.1007/978-3-319-63390-9_19},
}
[AT17] Rajeev Alur et Stavros Tripakis. Automatic Synthesis of Distributed Protocols. SIGACT News 48(1):55-90. ACM Press, mars 2017. 
@article{sigact-news48(1)-AT,
  author =              {Alur, Rajeev and Tripakis, Stavros},
  title =               {Automatic Synthesis of Distributed Protocols},
  publisher =           {ACM Press},
  journal =             {SIGACT News},
  volume =              {48},
  number =              {1},
  pages =               {55-90},
  year =                {2017},
  month =               mar,
  doi =                 {10.1145/3061640.3061652},
}
[BDG+17] Nathalie Bertrand, Miheer Dewaskar, Blaise Genest et Hugo Gimbert. Controlling a population. In CONCUR'17, Leibniz International Proceedings in Informatics 85, pages 12:1-12:16. Leibniz-Zentrum für Informatik, septembre 2017. 
@inproceedings{concur2017-BDGG,
  author =              {Bertrand, Nathalie and Dewaskar, Miheer and Genest,
                         Blaise and Gimbert, Hugo},
  title =               {Controlling a population},
  editor =              {Meyer, Roland and Nestmann, Uwe},
  booktitle =           {{P}roceedings of the 28th {I}nternational
                         {C}onference on {C}oncurrency {T}heory
                         ({CONCUR}'17)},
  acronym =             {{CONCUR}'17},
  publisher =           {Leibniz-Zentrum f{\"u}r Informatik},
  series =              {Leibniz International Proceedings in Informatics},
  volume =              {85},
  pages =               {12:1-12:16},
  year =                {2017},
  month =               sep,
  doi =                 {10.4230/LIPIcs.CONCUR.2017.12},
}
[BGG17] Nathalie Bertrand, Blaise Genest et Hugo Gimbert. Qualitative Determinacy and Decidability of Stochastic Games with Signals. Journal of the ACM 64(5):33:1-33:48. ACM Press, octobre 2017. 
@article{jacm64(5)-BGG,
  author =              {Bertrand, Nathalie and Genest, Blaise and Gimbert,
                         Hugo},
  title =               {Qualitative Determinacy and Decidability of
                         Stochastic Games with Signals},
  publisher =           {ACM Press},
  journal =             {Journal of the~ACM},
  volume =              {64},
  number =              {5},
  pages =               {33:1-33:48},
  year =                {2017},
  month =               oct,
  doi =                 {10.1145/3107926},
}
[BGH+17] Thomas Brihaye, Gilles Geeraerts, Axel Haddad et Benjamin Monmege. Pseudopolynomial iterative algorithm to solve total-payoff games and min-cost reachability game. Acta Informatica 54(1):85-125. Springer-Verlag, février 2017. 
@article{acta54(1)-BGHM,
  author =              {Brihaye, {\relax Th}omas and Geeraerts, Gilles and
                         Haddad, Axel and Monmege, Benjamin},
  title =               {Pseudopolynomial iterative algorithm to solve
                         total-payoff games and min-cost reachability game},
  publisher =           {Springer-Verlag},
  journal =             {Acta Informatica},
  volume =              {54},
  number =              {1},
  pages =               {85-125},
  year =                {2017},
  month =               feb,
  doi =                 {10.1007/s00236-016-0276-z},
}
[BHM17] Béatrice Bérard, Loïc Hélouët et John Mullins. Non-interference in partial order models. ACM Transactions on Embedded Computing Systems. ACM Press, 2017. À paraître. 
@article{tecs-BHM,
  author =              {B{\'e}rard, B{\'e}atrice and H{\'e}lou{\"e}t,
                         Lo{\"\i}c and Mullins, John},
  title =               {Non-interference in partial order models},
  publisher =           {ACM Press},
  journal =             {ACM Transactions on Embedded Computing Systems},
  year =                {2017},
  note =                {To~appear},
}
[BJM17] Patricia Bouyer, Vincent Jugé et Nicolas Markey. Courcelle's Theorem Made Dynamic. Technical Report 1702.05183, arXiv, février 2017.
Résumé

Dynamic complexity is concerned with updating the output of a problem when the input is slightly changed. We study the dynamic complexity of model checking a fixed monadic second-order formula over evolving subgraphs of a fixed maximal graph having bounded tree-width; here the subgraph evolves by losing or gaining edges (from the maximal graph). We show that this problem is in DynFO (with LOGSPACE precomputation), via a reduction to a Dyck reachability problem on an acyclic automaton.

@techreport{arxiv1702.05183-BJM,
  author =              {Bouyer, Patricia and Jug{\'e}, Vincent and Markey,
                         Nicolas},
  title =               {{C}ourcelle's Theorem Made Dynamic},
  number =              {1702.05183},
  year =                {2017},
  month =               feb,
  institution =         {arXiv},
  abstract =            {Dynamic complexity is concerned with updating the
                         output of a problem when the input is slightly
                         changed. We study the dynamic complexity of model
                         checking a fixed monadic second-order formula over
                         evolving subgraphs of a fixed maximal graph having
                         bounded tree-width; here the subgraph evolves by
                         losing or gaining edges (from the maximal graph).
                         We~show that this problem is in DynFO (with LOGSPACE
                         precomputation), via a reduction to a Dyck
                         reachability problem on an acyclic automaton.},
}
[BMM17] Raphaël Berthon, Bastien Maubert et Aniello Murano. Decidability Results for ATL* with Imperfect Information and Perfect Recall. In AAMAS'17, pages 1250-1258. International Foundation for Autonomous Agents and Multiagent Systems, mai 2017. 
@inproceedings{aamas2017-BMM,
  author =              {Berthon, Rapha{\"e}l and Maubert, Bastien and
                         Murano, Aniello},
  title =               {Decidability Results for {ATL\textsuperscript{*}}
                         with Imperfect Information and Perfect Recall},
  editor =              {Das, Sanmay and Durfee, Ed and Larson, Kate and
                         Winikoff, Michael},
  booktitle =           {{P}roceedings of the 16th {I}nternational
                         {C}onference on {A}utonomous {A}gents and
                         {M}ultiagent {S}ystems ({AAMAS}'17)},
  acronym =             {{AAMAS}'17},
  publisher =           {International Foundation for Autonomous Agents and
                         Multiagent Systems},
  pages =               {1250-1258},
  year =                {2017},
  month =               may,
}
[BMM+17] Raphaël Berthon, Bastien Maubert, Aniello Murano, Sasha Rubin et Moshe Y. Vardi. Strategy Logic with Imperfect Information. In LICS'17, pages 1-12. IEEE Comp. Soc. Press, juin 2017. 
@inproceedings{lics2017-BMMRV,
  author =              {Berthon, Rapha{\"e}l and Maubert, Bastien and
                         Murano, Aniello and Rubin, Sasha and Vardi, Moshe
                         Y.},
  title =               {Strategy Logic with Imperfect Information},
  booktitle =           {{P}roceedings of the 32nd {A}nnual {S}ymposium on
                         {L}ogic in {C}omputer {S}cience ({LICS}'17)},
  acronym =             {{LICS}'17},
  publisher =           {IEEE Comp. Soc. Press},
  pages =               {1-12},
  year =                {2017},
  month =               jun,
  doi =                 {10.1109/LICS.2017.8005136},
}
[BRS17] Romain Brenguier, Jean-François Raskin et Ocan Sankur. Assume-admissible synthesis. Acta Informatica 54(1):41-83. Springer-Verlag, février 2017. 
@article{acta54(1)-BRS,
  author =              {Brenguier, Romain and Raskin, Jean-Fran{\c c}ois and
                         Sankur, Ocan},
  title =               {Assume-admissible synthesis},
  publisher =           {Springer-Verlag},
  journal =             {Acta Informatica},
  volume =              {54},
  number =              {1},
  pages =               {41-83},
  year =                {2017},
  month =               feb,
  doi =                 {10.1007/s00236-016-0273-2},
}
[BW17] Julian C. Bradfield et Igor Walukiewicz. The mu-calculus and model-checking. In Edmund M. Clarke, Thomas A. Henzinger et Helmut Veith (eds.), Handbook of Model Checking. Springer-Verlag, 2017. À paraître. 
@incollection{HMC-BW,
  author =              {Bradfield, Julian C. and Walukiewicz, Igor},
  title =               {The mu-calculus and model-checking},
  editor =              {Clarke, Edmund M. and Henzinger, Thomas A. and
                         Veith, Helmut},
  booktitle =           {Handbook of Model Checking},
  publisher =           {Springer-Verlag},
  year =                {2017},
  note =                {To~appear},
}
[CDH17] Krishnendu Chatterjee, Laurent Doyen et Thomas A. Henzinger. The Cost of Exactness in Quantitative Reachability. In Models, Algorithms, Logics and Tools: Essays Dedicated to Kim Guldstrand Larsen on the Occasion of His 60th Birthday, Lecture Notes in Computer Science 10460, pages 367-381. Springer-Verlag, août 2017. 
@inproceedings{kimfest2017-CDH,
  author =              {Chatterjee, Krishnendu and Doyen, Laurent and
                         Henzinger, Thomas A.},
  title =               {The Cost of Exactness in Quantitative Reachability},
  editor =              {Aceto, Luca and Bacci, Giorgio and Bacci, Giovanni
                         and Ing{\'o}lfsd{\'o}ttir, Anna and Legay, Axel and
                         Mardare, Radu},
  booktitle =           {Models, Algorithms, Logics and Tools: Essays
                         Dedicated to Kim Guldstrand Larsen on the Occasion
                         of His 60th Birthday},
  publisher =           {Springer-Verlag},
  series =              {Lecture Notes in Computer Science},
  volume =              {10460},
  pages =               {367-381},
  year =                {2017},
  month =               aug,
  doi =                 {10.1007/978-3-319-63121-9_18},
}
[DKR+17] Manfred Droste, Temur Kutsia, George Rahonis et Wolfgang Schreiner. MK-fuzzy Automata and MSO Logics. In GandALF'17, Electronic Proceedings in Theoretical Computer Science 256, pages 106-120. Septembre 2017. 
@inproceedings{gandalf2017-DKRS,
  author =              {Droste, Manfred and Kutsia, Temur and Rahonis,
                         George and Schreiner, Wolfgang},
  title =               {{MK}-fuzzy Automata and {MSO} Logics},
  editor =              {Bouyer, Patricia and Orlandini, Andrea and
                         San{~}Pietro, Pierluigi},
  booktitle =           {{P}roceedings of the 8th {I}nternational {S}ymposium
                         on {G}ames, {A}utomata, {L}ogics and {F}ormal
                         {V}erification ({GandALF}'17)},
  acronym =             {{GandALF}'17},
  series =              {Electronic Proceedings in Theoretical Computer
                         Science},
  volume =              {256},
  pages =               {106-120},
  year =                {2017},
  month =               sep,
  doi =                 {10.4204/EPTCS.256.8},
}
[EGL+17] Javier Esparza, Pierre Ganty, Jérôme Leroux et Rupak Majumdar. Verification of Population Protocols. Acta Informatica 54(2):191-215. Springer-Verlag, mars 2017. 
@article{atca54(2)-EGLM,
  author =              {Esparza, Javier and Ganty, Pierre and Leroux,
                         J{\'e}r{\^o}me and Majumdar, Rupak},
  title =               {Verification of Population Protocols},
  publisher =           {Springer-Verlag},
  journal =             {Acta Informatica},
  volume =              {54},
  number =              {2},
  pages =               {191-215},
  year =                {2017},
  month =               mar,
  doi =                 {10.1007/s00236-016-0272-3},
}
[Gar17] Patrick Gardy. Semantics of Strategy Logic. PhD thesis, Lab. Spécification & Vérification, Univ. Paris-Saclay, France, Juin 2017. 
@phdthesis{phd-gardy,
  author =              {Gardy, Patrick},
  title =               {Semantics of Strategy Logic},
  year =                {2017},
  month =               jun,
  school =              {Lab.~Sp\'ecification \& V\'erification, Univ.
                         Paris-Saclay, France},
  type =                {{PhD} thesis},
}
[GBB+17] Mauricio González, Olivier Beaude, Patricia Bouyer, Samson Lasaulce et Nicolas Markey. Stratégies d'ordonnancement de consommation d'énergie en présence d'information imparfaite de prévision. In GRETSI'17. Septembre 2017.
Résumé

Energy consumption problems (e.g., electric vehicles charging) are very related to communication problems. The "water-filling" algorithm can be used, but it is not robust w.r.t. the noise of the "non-flexible", i.e. not-controllable, energy consumption forecasting. We propose a robust algorithm using the probabilistic model-checker PRISM, to exploit the idea of discretizing the consumption action (as for a modulation to small constellation) and the dynamic structure of the problem in a Markov-decision-process model.

@inproceedings{gretsi2017-GBBLM,
  author =              {Gonz{\'a}lez, Mauricio and Beaude, Olivier and
                         Bouyer, Patricia and Lasaulce, Samson and Markey,
                         Nicolas},
  title =               {Strat{\'e}gies d'ordonnancement de consommation
                         d'{\'e}nergie en pr{\'e}sence d'information
                         imparfaite de pr{\'e}vision},
  booktitle =           {{A}ctes du 26{\`e}me {C}olloque du {G}roupe
                         d'{\'E}tudes du {T}raitement du {S}ignal et des
                         {I}mages ({GRETSI}'17)},
  acronym =             {{GRETSI}'17},
  year =                {2017},
  month =               sep,
  abstract =            {Energy consumption problems (e.g., electric vehicles
                         charging) are very related to communication
                         problems. The "water-filling" algorithm can be used,
                         but it is not robust w.r.t. the noise of the
                         "non-flexible", i.e. not-controllable, energy
                         consumption forecasting. We~propose a robust
                         algorithm using the probabilistic model-checker
                         PRISM, to exploit the idea of discretizing the
                         consumption action (as~for a modulation to small
                         constellation) and the dynamic structure of the
                         problem in a Markov-decision-process model.},
}
[GHP+17] Julian Gutierrez, Paul Harrenstein, Giuseppe Perelli et Michael Wooldridge. Nash Equilibrium and Bisimulation Invariance. In CONCUR'17, Leibniz International Proceedings in Informatics 85, pages 17:1-17:16. Leibniz-Zentrum für Informatik, septembre 2017. 
@inproceedings{concur2017-GHPW,
  author =              {Gutierrez, Julian and Harrenstein, Paul and Perelli,
                         Giuseppe and Wooldridge, Michael},
  title =               {{N}ash Equilibrium and Bisimulation Invariance},
  editor =              {Meyer, Roland and Nestmann, Uwe},
  booktitle =           {{P}roceedings of the 28th {I}nternational
                         {C}onference on {C}oncurrency {T}heory
                         ({CONCUR}'17)},
  acronym =             {{CONCUR}'17},
  publisher =           {Leibniz-Zentrum f{\"u}r Informatik},
  series =              {Leibniz International Proceedings in Informatics},
  volume =              {85},
  pages =               {17:1-17:16},
  year =                {2017},
  month =               sep,
  doi =                 {10.4230/LIPIcs.CONCUR.2017.17},
}
[JBB+17] Swen Jacobs, Roderick Bloem, Romain Brenguier, Rüdiger Ehlers, Timotheus Hell, Robert Könighofer, Guillermo A. Pérez, Jean-François Raskin, Leonid Ryzhyk, Ocan Sankur, Martin Seidl, Leander Tentrup et Adam Walker. The first reactive synthesis competition (SYNTCOMP 2014). International Journal on Software Tools for Technology Transfer 19(3):367-390. Springer-Verlag, juin 2017. 
@article{sttt19(3)-JBBEHKPRRSSTW,
  author =              {Jacobs, Swen and Bloem, Roderick and Brenguier,
                         Romain and Ehlers, R{\"u}diger and Hell, Timotheus
                         and K{\"o}nighofer, Robert and P{\'e}rez, Guillermo
                         A. and Raskin, Jean-Fran{\c c}ois and Ryzhyk, Leonid
                         and Sankur, Ocan and Seidl, Martin and Tentrup,
                         Leander and Walker, Adam},
  title =               {The first reactive synthesis competition
                         ({SYNTCOMP}~2014)},
  publisher =           {Springer-Verlag},
  journal =             {International Journal on Software Tools for
                         Technology Transfer},
  volume =              {19},
  number =              {3},
  pages =               {367-390},
  year =                {2017},
  month =               jun,
  doi =                 {10.1007/s10009-016-0416-3},
}
[MMP+17] Fabio Mogavero, Aniello Murano, Giuseppe Perelli et Moshe Y. Vardi. Reasoning About Strategies: On the Satisfiability Problem. Logical Methods in Computer Science 13(1). Mars 2017. 
@article{lmcs13(1)-MMPV,
  author =              {Mogavero, Fabio and Murano, Aniello and Perelli,
                         Giuseppe and Vardi, Moshe Y.},
  title =               {Reasoning About Strategies: On~the~Satisfiability
                         Problem},
  journal =             {Logical Methods in Computer Science},
  volume =              {13},
  number =              {1},
  year =                {2017},
  month =               mar,
  doi =                 {10.23638/LMCS-13(1:9)2017},
}
[RPV17] Nima Roohi, Pavithra Prabhakar et Mahesh Viswanathan. Robust model checking of timed automata under clock drifts. In HSCC'17, pages 153-162. ACM Press, avril 2017. 
@inproceedings{hscc2017-RPV,
  author =              {Roohi, Nima and Prabhakar, Pavithra and Viswanathan,
                         Mahesh},
  title =               {Robust model checking of timed automata under clock
                         drifts},
  editor =              {Frehse, Goran and Mitra, Sayan},
  booktitle =           {{P}roceedings of the 20th {I}nternational {W}orkshop
                         on {H}ybrid {S}ystems: {C}omputation and {C}ontrol
                         ({HSCC}'14)},
  acronym =             {{HSCC}'17},
  publisher =           {ACM Press},
  pages =               {153-162},
  year =                {2017},
  month =               apr,
  doi =                 {10.1145/3049797.3049821},
}
[ST17] Ocan Sankur et Jean-Pierre Talpin. An Abstraction Technique For Parameterized Model Checking of Leader Election Protocols: Application to FTSP. In TACAS'17, Lecture Notes in Computer Science 10205. Springer-Verlag, avril 2017. 
@inproceedings{tacas2017-ST,
  author =              {Sankur, Ocan and Talpin, Jean-Pierre},
  title =               {An~Abstraction Technique For Parameterized Model
                         Checking of Leader Election Protocols: Application
                         to~{FTSP}},
  editor =              {Legay, Axel and Margaria, Tiziana},
  booktitle =           {{P}roceedings of the 23rd {I}nternational
                         {C}onference on {T}ools and {A}lgorithms for
                         {C}onstruction and {A}nalysis of {S}ystems
                         ({TACAS}'17)~-- {P}art~{I}},
  acronym =             {{TACAS}'17},
  publisher =           {Springer-Verlag},
  series =              {Lecture Notes in Computer Science},
  volume =              {10205},
  year =                {2017},
  month =               apr,
  doi =                 {10.1007/978-3-662-54577-5_2},
}
[Sta17] Daniel Stan. Randomized strategies in concurrent games. Thèse de doctorat, Lab. Spécification & Vérification, ENS Cachan, France, Mars 2017. 
@phdthesis{phd-stan,
  author =              {Stan, Daniel},
  title =               {Randomized strategies in concurrent games},
  year =                {2017},
  month =               mar,
  school =              {Lab.~Sp\'ecification \& V\'erification, ENS Cachan,
                         France},
  type =                {Th\`ese de doctorat},
}
[TM17] Tamás Tóth et István Majzik. Lazy reachability checking for timed automata using interpolants. In FORMATS'17, Lecture Notes in Computer Science 10419, pages 264-280. Springer-Verlag, septembre 2017. 
@inproceedings{formats2017-TM,
  author =              {T{\'o}th, Tam{\'a}s and Majzik, Istv{\'a}n},
  title =               {Lazy reachability checking for timed automata using
                         interpolants},
  editor =              {Abate, Alessandro and Geeraerts, Gilles},
  booktitle =           {{P}roceedings of the 15th {I}nternational
                         {C}onferences on {F}ormal {M}odelling and {A}nalysis
                         of {T}imed {S}ystems ({FORMATS}'17)},
  acronym =             {{FORMATS}'17},
  publisher =           {Springer-Verlag},
  series =              {Lecture Notes in Computer Science},
  volume =              {10419},
  pages =               {264-280},
  year =                {2017},
  month =               sep,
  doi =                 {10.1007/978-3-319-65765-3_15},
}
Liste des auteurs