Nicolas Markey

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.

@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.},
}

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.

@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.},
}

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.

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.},
}

Abstract

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.},
}

@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},
}

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.

@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.},
}

@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},
}

@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},
}

@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},
}

@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},
}

@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},
}

@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},
}

@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},
}

@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},
}

@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},
}

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.

@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.},
}

@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,
}

@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},
}

@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},
}

@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},
}

@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},
}

@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},
}

@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},
}

@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},
}

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.

@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.},
}

@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},
}

@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},
}

@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},
}

@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},
}

@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},
}

@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},
}

@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},
}