Nicolas Markey

Abstract

Synchronizing a (deterministic, finite-state) automaton is the problem of finding a sequence of actions to be played in the automaton in order to end up in the same state independently of the starting state. We consider synchronization with LTL constraints on the executions leading to synchronization, extending the results of [Petra Wolf. Synchronization under dynamic constraints. FSTTCS'20] by showing that the problem is PSPACE-complete for LTL as well as for restricted fragments (involving only modality F or G), while it is NP-complete for constraints expressed using only modality X.

@article{ipl182()-BFM,
  author =              {Bertrand, Nathalie and Francon, Hugo and Markey,
                         Nicolas},
  title =               {Synchronizing words under {LTL} constraints},
  publisher =           {Elsevier},
  journal =             {Information Processing Letters},
  volume =              {182},
  year =                {2023},
  month =               aug,
  doi =                 {10.1016/j.ipl.2023.106392},
  abstract =            {Synchronizing a (deterministic, finite-state)
                         automaton is the problem of finding a sequence of
                         actions to be played in the automaton in order to
                         end up in the same state independently of the
                         starting state. We~consider synchronization
                         with~\textsf{LTL} constraints on the executions
                         leading to synchronization, extending the results
                         of~[Petra~Wolf. Synchronization under dynamic
                         constraints. FSTTCS'20] by~showing that the problem
                         is \textsf{PSPACE}-complete for~\textsf{LTL} as well
                         as for restricted fragments (involving only
                         modality~\textsf{F} or~\textsf{G}), while it is
                         \textsf{NP}-complete for constraints expressed using
                         only modality~\textsf{X}.},
}

Abstract

Temporal logics are extensively used for the specification of on-going behaviors of computer systems. Two significant developments in this area are the extension of traditional temporal logics with modalities that enable the specification of on-going strategic behaviors in multi-agent systems, and the transition of temporal logics to a quantitative setting, where different satisfaction values enable the specifier to formalize concepts such as certainty or quality. In the first class, SL (Strategy Logic) is one of the most natural and expressive logics describing strategic behaviors. In the second class, a notable logic is LTL[F], which extends LTL with quality operators.

In this work we introduce and study SL[F], which enables the specification of quantitative strategic behaviors. The satisfaction value of an SL[F] formula is a real value in [0,1], reflecting "how much" or "how well" the strategic on-going objectives of the underlying agents are satisfied. We demonstrate the applications of SL[F] in quantitative reasoning about multi-agent systems, showing how it can express and measure concepts like stability in multi-agent systems, and how it generalizes some fuzzy temporal logics. We also provide a model-checking algorithm for SL[F], based on a quantitative extension of Quantified CTL*. Our algorithm provides the first decidability result for a quantitative extension of Strategy Logic. In addition, it can be used for synthesizing strategies that maximize the quality of the systems' behavior

@article{tocl24(3)-BKMMMP,
  author =              {Bouyer, Patricia and Kupferman, Orna and Markey,
                         Nicolas and Maubert, Bastien and Murano, Aniello and
                         Perelli, Giuseppe},
  title =               {Reasoning about Quality and Fuzziness of Strategic
                         Behaviours},
  publisher =           {ACM Press},
  journal =             {ACM Transactions on Computational Logic},
  volume =              {24},
  number =              {3},
  pages =               {21:1-21:38},
  year =                {2023},
  month =               jul,
  doi =                 {10.1145/3582498},
  abstract =            {Temporal logics are extensively used for the
                         specification of on-going behaviors of computer
                         systems. Two significant developments in this area
                         are the extension of traditional temporal logics
                         with modalities that enable the specification of
                         on-going strategic behaviors in multi-agent systems,
                         and the transition of temporal logics to a
                         quantitative setting, where different satisfaction
                         values enable the specifier to formalize concepts
                         such as certainty or quality. In~the first class,
                         SL~(Strategy~Logic)~is one of the most natural and
                         expressive logics describing strategic behaviors. In
                         the second class, a notable logic is
                         \(\textsf{LTL}[\mathcal{F}]\), which extends
                         \textsf{LTL} with quality operators. \par In~this
                         work we introduce and study
                         \(\textsf{SL}[\mathcal{F}]\), which enables the
                         specification of quantitative strategic behaviors.
                         The satisfaction value of an
                         \(\textsf{SL}[\mathcal{F}]\) formula is a real value
                         in \([0,1]\), reflecting {"}how~much{"} or
                         {"}how~well{"} the strategic on-going objectives of
                         the underlying agents are satisfied. We demonstrate
                         the applications of \(\textsf{SL}[\mathcal{F}]\) in
                         quantitative reasoning about multi-agent systems,
                         showing how it can express and measure concepts like
                         stability in multi-agent systems, and how it
                         generalizes some fuzzy temporal logics. We also
                         provide a model-checking algorithm for
                         \(\textsf{SL}[\mathcal{F}]\), based on a
                         quantitative extension of
                         Quantified~\(\textsf{CTL}^*\). Our~algorithm
                         provides the first decidability result for a
                         quantitative extension of Strategy Logic. In
                         addition, it can be used for synthesizing strategies
                         that maximize the quality of the systems' behavior},
}

Abstract

Network congestion games are a simple model for reasoning about routing problems in a network. They are a very popular topic in algorithmic game theory, and a huge amount of results about existence and (in)efficiency of equilibrium strategy profiles in those games have been obtained over the last 20 years.

In particular, the price of anarchy has been defined as an important notion for measuring the inefficiency of Nash equilibria. Generic bounds have been obtained for the price of anarchy over various classes of networks, but little attention has been put on the effective computation of this value for a given network. This talk presents recent results on this problem in different settings.

@inproceedings{formats2023-Mar,
  author =              {Markey, Nicolas},
  title =               {Computing the price of anarchy in atomic network
                         congestion games (invited~talk)},
  editor =              {Petrucci, Laure and Sproston, Jeremy},
  booktitle =           {{P}roceedings of the 21st {I}nternational
                         {C}onferences on {F}ormal {M}odelling and {A}nalysis
                         of {T}imed {S}ystems ({FORMATS}'23)},
  acronym =             {{FORMATS}'23},
  publisher =           {Springer-Verlag},
  series =              {Lecture Notes in Computer Science},
  volume =              {14138},
  pages =               {3-12},
  year =                {2023},
  month =               sep,
  doi =                 {10.1007/978-3-031-42626-1_1},
  abstract =            {Network congestion games are a simple model for
                         reasoning about routing problems in a network. They
                         are a very popular topic in algorithmic game theory,
                         and a huge amount of results about existence and
                         (in)efficiency of equilibrium strategy profiles in
                         those games have been obtained over the last
                         20~years. \par In~particular, the price of anarchy
                         has been defined as an important notion for
                         measuring the inefficiency of Nash equilibria.
                         Generic bounds have been obtained for the price of
                         anarchy over various classes of networks, but little
                         attention has been put on the effective computation
                         of this value for a given network. This talk
                         presents recent results on this problem in different
                         settings.},
}

@patent{EP4064057B1,
  author =              {Noguchi, Reiya and J{\'e}ron, Thierry and Markey,
                         Nicolas and Sankur, Ocan},
  title =               {Method and system for correcting the operation of a
                         target computer system by using timed requirements},
  number =              {EP 4 064 057 B1},
  year =                {2023},
  month =               jul,
}

@inproceedings{fsttcs2023-AAB,
  author =              {Almagor, Shaull and Assa, Daniel and Boker, Udi},
  title =               {Synchronized {CTL} over One-Counter Automata},
  editor =              {Bouyer, Patricia and Srinivasan, Srikanth},
  booktitle =           {{P}roceedings of the 43rd {C}onference on
                         {F}oundations of {S}oftware {T}echnology and
                         {T}heoretical {C}omputer {S}cience ({FSTTCS}'23)},
  acronym =             {{FSTTCS}'23},
  publisher =           {Leibniz-Zentrum f{\"u}r Informatik},
  series =              {Leibniz International Proceedings in Informatics},
  volume =              {284},
  pages =               {19:1-19:22},
  year =                {2023},
  month =               dec,
  doi =                 {10.4230/LIPIcs.FSTTCS.2023.19},
}

@article{siglog-news35()-BL,
  author =              {Boker, Udi and Lehtinen, Karoliina},
  title =               {When a Little Nondeterminism Goes a Long Way: an
                         Introduction to History-Determinism},
  publisher =           {ACM Press},
  journal =             {SIGLOG News},
  volume =              {35},
  pages =               {24-51},
  year =                {2023},
  month =               jan,
}

@article{mathprog-CDS,
  author =              {Cominetti, Roberto and Dose, Valerio and Scarsini,
                         Marco},
  title =               {The~price of anarchy in routing games as a function
                         of the demand},
  journal =             {Mathematical Programming},
  year =                {2023},
  doi =                 {10.1007/s10107-021-01701-7},
  note =                {To~appear},
}

@techreport{GoG-fij23,
  author =              {Fijalkow, Nathana{\"e}l and Bertrand, Nathalie and
                         Bouyer, Patricia and Brenguier, Romain and Carayol,
                         Arnaud and Fearnley, John and Gimbert, Hugo an Horn,
                         Florian and Ibsen{-}Jensen, Rasmus and Markey,
                         Nicolas and Monmege, Benjamin and Novotn{\'y}, Petr
                         and Randour, Mickael and Sankur, Ocan and Schmitz,
                         Sylvain and Serre, Olivier and Skomra, Mateusz},
  title =               {Games on graphs},
  number =              {2305.10546},
  year =                {2023},
  month =               may,
  institution =         {arXiv},
}

@phdthesis{phd-ganguly,
  author =              {Ganguly, Ritam},
  title =               {Runtime verification of distributed systems},
  year =                {2023},
  school =              {Michigan State University, USA},
  type =                {{PhD} thesis},
}

@inproceedings{csl2023-HK,
  author =              {Hazard, {\'E}mile and Kuperberg, Denis},
  title =               {Explorable automata},
  editor =              {Klin, Bartek and Pimentel, Elaine},
  booktitle =           {{P}roceedings of the 31st {EACSL} {A}nnual
                         {C}onference on {C}omputer {S}cience {L}ogic
                         ({CSL}'23)},
  acronym =             {{CSL}'23},
  publisher =           {Leibniz-Zentrum f{\"u}r Informatik},
  series =              {Leibniz International Proceedings in Informatics},
  volume =              {252},
  pages =               {24:1-24:18},
  year =                {2023},
  month =               feb,
  doi =                 {10.4230/LIPIcs.CSL.2023.24},
}

@article{mathprog199(1)-WMRX,
  author =              {Wu, Zijun and M{\"o}hring, Rolf H. and Ren, Chunying
                         and Xu, Dachaun},
  title =               {A~convergence analysis of the price of anarchy in
                         atomic congestion games},
  journal =             {Mathematical Programming},
  volume =              {199},
  number =              {1},
  pages =               {937-993},
  year =                {2023},
  month =               may,
  doi =                 {10.1007/s10107-022-01853-0},
}