Nicolas Markey

Abstract

We introduce and study SL[F]—a quantitative extension of SL (Strategy Logic), one of the most natural and expressive logics describing strategic behaviours. 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, by showing how it can express concepts of stability in multi-agent systems, and how it generalises some fuzzy temporal logics. We also provide a model-checking algorithm for our logic, based on a quantitative extension of Quantified CTL.

@inproceedings{ijcai2019-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},
  editor =              {Kraus, Sarit},
  booktitle =           {{P}roceedings of the 28th {I}nternational {J}oint
                         {C}onference on {A}rtificial {I}ntelligence
                         ({IJCAI}'19)},
  acronym =             {{IJCAI}'19},
  publisher =           {IJCAI organization},
  pages =               {1588-1594},
  year =                {2019},
  month =               aug,
  doi =                 {10.24963/ijcai.2019/220},
  abstract =            {We~introduce and study
                         {\(\textsf{SL}[\mathcal{F}]\)}---a~quantitative
                         extension of {\(\textsf{SL}\)} (Strategy Logic),
                         one~of the most natural and expressive logics
                         describing strategic behaviours. 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, by showing how
                         it can express concepts of stability in multi-agent
                         systems, and how it generalises some fuzzy temporal
                         logics. We~also provide a model-checking algorithm
                         for our logic, based on a quantitative extension of
                         Quantified~\textsf{CTL}.},
}

Abstract

We study games with reachability objectives under energy constraints. We first prove that under strict energy constraints (either only lower-bound constraint or interval constraint), those games are LOGSPACE-equivalent to energy games with the same energy constraints but without reachability objective (i.e., for infinite runs). We then consider two kinds of relaxations of the upper-bound constraints (while keeping the lower-bound constraint strict): in the first one, called weak upper bound, the upper bound is absorbing, in the sense that it allows receiving more energy when the upper bound is already reached, but the extra energy will not be stored; in the second one, we allow for temporary violations of the upper bound, imposing limits on the number or on the amount of violations.

We prove that when considering weak upper bound, reachability objectives require memory, but can still be solved in polynomial-time for one-player arenas; we prove that they are in coNP in the two-player setting. Allowing for bounded violations makes the problem PSPACE-complete for one-player arenas and EXPTIME-complete for two players.

@inproceedings{gandalf2019-HMR,
  author =              {H{\'e}lou{\"e}t, Lo{\"\i}c and Markey, Nicolas and
                         Raha, Ritam},
  title =               {Reachability games with relaxed energy constraints},
  editor =              {Leroux, J{\'e}r{\^o}me and Raskin, Jean-Fran{\c
                         c}ois},
  booktitle =           {{P}roceedings of the 10th {I}nternational
                         {S}ymposium on {G}ames, {A}utomata, {L}ogics and
                         {F}ormal {V}erification ({GandALF}'19)},
  acronym =             {{GandALF}'19},
  series =              {Electronic Proceedings in Theoretical Computer
                         Science},
  volume =              {305},
  pages =               {17-33},
  year =                {2019},
  month =               sep,
  doi =                 {10.4204/EPTCS.305.2},
  abstract =            {We study games with reachability objectives under
                         energy constraints. We first prove that under strict
                         energy constraints (either only lower-bound
                         constraint or interval constraint), those games are
                         \textsf{LOGSPACE}-equivalent to energy games with
                         the same energy constraints but without reachability
                         objective (i.e., for infinite runs). We then
                         consider two kinds of relaxations of the upper-bound
                         constraints (while keeping the lower-bound
                         constraint strict): in the first one, called
                         \emph{weak upper bound}, the upper bound is
                         \emph{absorbing}, in the sense that it allows
                         receiving more energy when the upper bound is
                         already reached, but the extra energy will not be
                         stored; in~the second~one, we~allow for
                         \emph{temporary violations} of the upper bound,
                         imposing limits on the number or on the amount of
                         violations.\par We prove that when considering weak
                         upper bound, reachability objectives require memory,
                         but can still be solved in polynomial-time for
                         one-player arenas; we prove that they are in
                         \textsf{coNP} in the two-player setting. Allowing
                         for bounded violations makes the problem
                         \textsf{PSPACE}-complete for one-player arenas and
                         \textsf{EXPTIME}-complete for two players.},
}

Abstract

We present abstraction-refinement algorithms for model checking safety properties of timed automata. The abstraction domain we consider abstracts away zones by restricting the set of clock constraints that can be used to define them, while the refinement procedure computes the set of constraints that must be taken into consideration in the abstraction so as to exclude a given spurious counterexample. We implement this idea in two ways: an enumerative algorithm where a lazy abstraction approach is adopted, meaning that possibly different abstract domains are assigned to each exploration node; and a symbolic algorithm where the abstract transition system is encoded with Boolean formulas.

@inproceedings{cav2019-RSM,
  author =              {Roussanaly, Victor and Sankur, Ocan and Markey,
                         Nicolas},
  title =               {Abstraction Refinement Algorithms for Timed
                         Automata},
  editor =              {Dillig, I{\c s}il and Ta{\c s}iran, Serdar},
  booktitle =           {{P}roceedings of the 31st {I}nternational
                         {C}onference on {C}omputer {A}ided {V}erification
                         ({CAV}'19)},
  acronym =             {{CAV}'19},
  publisher =           {Springer-Verlag},
  series =              {Lecture Notes in Computer Science},
  volume =              {11561},
  pages =               {22-40},
  year =                {2019},
  month =               jul,
  doi =                 {10.1007/978-3-030-25540-4_2},
  abstract =            {We~present abstraction-refinement algorithms for
                         model checking safety properties of timed automata.
                         The~abstraction domain we consider abstracts away
                         zones by restricting the set of clock constraints
                         that can be used to define them, while the
                         refinement procedure computes the set of constraints
                         that must be taken into consideration in the
                         abstraction so as to exclude a given spurious
                         counterexample. We~implement this idea in two~ways:
                         an~enumerative algorithm where a lazy abstraction
                         approach is adopted, meaning that possibly different
                         abstract domains are assigned to each exploration
                         node; and a symbolic algorithm where the abstract
                         transition system is encoded with Boolean formulas.},
}

@inproceedings{concur2019-BBGRB,
  author =              {Brihaye, {\relax Th}omas and Bruy{\`e}re,
                         V{\'e}ronique and Goeminne, Aline and Raskin,
                         Jean-Fran{\c c}ois and Van{~}den{ }Bogaard, Marie},
  title =               {The~Complexity of Subgame Perfect Equilibria in
                         Quantitative Reachability Games},
  editor =              {Fokkink, Wan J. and van Glabbeek, Rob},
  booktitle =           {{P}roceedings of the 30th {I}nternational
                         {C}onference on {C}oncurrency {T}heory
                         ({CONCUR}'19)},
  acronym =             {{CONCUR}'19},
  publisher =           {Leibniz-Zentrum f{\"u}r Informatik},
  series =              {Leibniz International Proceedings in Informatics},
  volume =              {140},
  pages =               {13:1-13:16},
  year =                {2019},
  month =               aug,
  doi =                 {10.4230/LIPIcs.CONCUR.2019.13},
}

@inproceedings{cav2019-BMRS,
  author =              {Busatto-Gaston, Damien and Monmege, Benjamin and
                         Reynier, Pierre-Alain and Sankur, Ocan},
  title =               {Robust Controller Synthesis in Timed B{\"u}chi
                         Automata: A~Symbolic Approach},
  editor =              {Dillig, I{\c s}il and Ta{\c s}iran, Serdar},
  booktitle =           {{P}roceedings of the 31st {I}nternational
                         {C}onference on {C}omputer {A}ided {V}erification
                         ({CAV}'19)},
  acronym =             {{CAV}'19},
  publisher =           {Springer-Verlag},
  series =              {Lecture Notes in Computer Science},
  volume =              {11561},
  pages =               {572-590},
  year =                {2019},
  month =               jul,
  doi =                 {10.1007/978-3-030-25540-4_33},
}

@inproceedings{concur2019-BL,
  author =              {Boker, Udi and Lehtinen, Karoliina},
  title =               {Good-for-game Automata: from Non-determinism to
                         Alternation},
  editor =              {Fokkink, Wan J. and van Glabbeek, Rob},
  booktitle =           {{P}roceedings of the 30th {I}nternational
                         {C}onference on {C}oncurrency {T}heory
                         ({CONCUR}'19)},
  acronym =             {{CONCUR}'19},
  publisher =           {Leibniz-Zentrum f{\"u}r Informatik},
  series =              {Leibniz International Proceedings in Informatics},
  volume =              {140},
  pages =               {19:1-19:16},
  year =                {2019},
  month =               aug,
  doi =                 {10.4230/LIPIcs.CONCUR.2019.19},
}

@article{moor44(4)-CJKU,
  author =              {Correa, Jos{\'e} R. and de~Jong, Jasper and
                         de~Keizer, Bart and Uetz, Marc},
  title =               {The inefficiency of {N}ash and subgame-perfect
                         equilibria for network routing},
  publisher =           {Informs},
  journal =             {Mathematics of Operations Research},
  volume =              {44},
  number =              {4},
  pages =               {1286-1303},
  year =                {2019},
  month =               nov,
  doi =                 {10.1287/moor.2018.0968},
}

@article{jcss100()-DMS,
  author =              {Doyen, Laurent and Massart, {\relax Th}ierry and
                         Shirmohammadi, Mahsa},
  title =               {The complexity of synchronizing {M}arkov decision
                         processes},
  publisher =           {Elsevier},
  journal =             {Journal of Computer and System Sciences},
  volume =              {100},
  pages =               {96-129},
  year =                {2019},
  month =               mar,
  doi =                 {10.1016/j.jcss.2018.09.004},
}

@inproceedings{mfcs2019-FGHHVW,
  author =              {Fernau, Henning and Gusev, Vladimir V. and Hoffmann,
                         Stefan and Holzer, Markus and Volkov, Mikhail V. and
                         Wolf, Petra},
  title =               {Computational Complexity of Synchronization under
                         Regular Constraints},
  editor =              {Rossmanith, Peter and Heggernes, Pinar and Katoen,
                         Joost-Pieter},
  booktitle =           {{P}roceedings of the 44th {I}nternational
                         {S}ymposium on {M}athematical {F}oundations of
                         {C}omputer {S}cience ({MFCS}'19)},
  acronym =             {{MFCS}'19},
  publisher =           {Leibniz-Zentrum f{\"u}r Informatik},
  series =              {Leibniz International Proceedings in Informatics},
  volume =              {138},
  pages =               {63:1-63:14},
  year =                {2019},
  month =               aug,
  doi =                 {10.4230/LIPIcs.MFCS.2019.63},
}

Abstract

This article focuses on the existence and synthesis of strategies in double-weighted Markov decision processes, which satisfy both a probability constraint over a weighted reachability condition, and a quantitative constraint on the expected value of a random variable defined using another reachability condition. This work generalizes a scheduling problem for energy consumption (typically the problem of charging electric vehicles). We study the set of values of a parameter (a threshold) for which the problem has a solution, and show how a partial characterization of this set can be obtained via two sequences of optimization problems. We also discuss the completeness and feasibility of the resulting approach.

@inproceedings{gretsi2019-GBLM,
  author =              {Gonz{\'a}lez, Mauricio and Bouyer, Patricia and
                         Lasaulce, Samson and Markey, Nicolas},
  title =               {Optimisation en pr\'esence de contraintes en
                         probabilit\'es et processus markoviens
                         contr\^ol\'es},
  booktitle =           {{A}ctes du 27{\`e}me {C}olloque du {G}roupe
                         d'{\'E}tudes du {T}raitement du {S}ignal et des
                         {I}mages ({GRETSI}'19)},
  acronym =             {{GRETSI}'19},
  year =                {2019},
  month =               aug,
  abstract =            {This article focuses on the existence and synthesis
                         of strategies in double-weighted Markov decision
                         processes, which satisfy both a probability
                         constraint over a weighted reachability condition,
                         and a quantitative constraint on the expected value
                         of a random variable defined using another
                         reachability condition. This work generalizes a
                         scheduling problem for energy consumption (typically
                         the problem of charging electric vehicles). We~study
                         the set of values of a parameter (a~threshold) for
                         which the problem has a solution, and show how a
                         partial characterization of this set can be obtained
                         via two sequences of optimization problems. We~also
                         discuss the completeness and feasibility of the
                         resulting approach.},
}

@phdthesis{phd-jaziri,
  author =              {Jaziri, Samy},
  title =               {Automata on timed structures},
  year =                {2019},
  month =               sep,
  school =              {{\'E}cole Normale Sup{\'e}rieure de Cachan, France},
}

@article{mscs29(1)-KMS,
  author =              {Knight, Sophia and Maubert, Bastien and
                         Schwarzentruber, Fran{\c c}ois},
  title =               {Reasoning about knowledge and messages in
                         asynchronous multi-agent systems},
  journal =             {Mathematical Structures in Computer Science},
  volume =              {29},
  number =              {1},
  pages =               {127-168},
  year =                {2019},
  month =               jan,
  doi =                 {10.1017/S0960129517000214},
}

@inproceedings{re2019-LDWHP,
  author =              {Langenfeld, Vincent and Dietsch, Daniel and
                         Westphal, Bernd and Hoenicke, Jochen and Post,
                         Amalinda},
  title =               {Scalable Analysis of Real-Time Requirements},
  editor =              {Damian, Daniela E. and Perini, Anna and Lee,
                         Seok-Won},
  booktitle =           {{P}roceedings of the 27th {I}nternaitonal
                         {R}equirements Engineering {C}onference ({RE}'19)},
  acronym =             {{RE}'19},
  publisher =           {IEEE Comp. Soc. Press},
  pages =               {234-244},
  year =                {2019},
  month =               sep,
  doi =                 {10.1109/RE.2019.00033},
}

@inproceedings{ijcai2019-MPS,
  author =              {Maubert, Bastien and Pinchinat, Sophie and
                         Schwarzentruber, Fran{\c c}ois},
  title =               {Reachability Games in Dynamic Epistemic Logic},
  editor =              {Kraus, Sarit},
  booktitle =           {{P}roceedings of the 28th {I}nternational {J}oint
                         {C}onference on {A}rtificial {I}ntelligence
                         ({IJCAI}'19)},
  acronym =             {{IJCAI}'19},
  publisher =           {IJCAI organization},
  pages =               {499-505},
  year =                {2019},
  month =               aug,
  doi =                 {10.24963/ijcai.2019/71},
}

@article{jalc24(2-4)-Nic,
  author =              {Nicaud, Cyril},
  title =               {The {{\v{C}}}ern{\'y} conjecture holds with high
                         probability},
  journal =             {Journal of Automata, Languages and Combinatorics},
  volume =              {24},
  number =              {2-4},
  pages =               {343-365},
  year =                {2019},
  doi =                 {10.25596/jalc-2019-343},
}

@article{tocl20(2)-QS,
  author =              {Quaas, Karin and Shirmohammadi, Mahsa},
  title =               {Synchronizing Data Words for Register Automata},
  publisher =           {ACM Press},
  journal =             {ACM Transactions on Computational Logic},
  volume =              {20},
  number =              {2},
  pages =               {11:1-11:27},
  year =                {2019},
  month =               apr,
  doi =                 {10.1145/3309760},
}

@article{jalc24(2-4)-Shi,
  author =              {Shitov, Yaroslav},
  title =               {An Improvement to a Recent Upper Bound for
                         Synchronizing Words of Finite Automata},
  journal =             {Journal of Automata, Languages and Combinatorics},
  volume =              {24},
  number =              {2-4},
  pages =               {367-373},
  year =                {2019},
  doi =                 {10.25596/jalc-2019-367},
}

@phdthesis{phd-sickert,
  author =              {Sickert, Salomon},
  title =               {A~unified translation of Linear Temporal Logic to
                         {\(\omega\)}-automata},
  year =                {2019},
  month =               jul,
  school =              {Technischen Universit{\"a}t M{\"u}nchen, Germany},
}