2022
[HJM22] Léo Henry, Thierry Jéron, and Nicolas Markey. Control strategies for off-line testing of timed systems. Formal Methods in System Design 60(2):147-194. Springer-Verlag, April 2022.
Abstract

Partial observability and controllability are two well-known issues in test-case synthesis for reactive systems. We address the problem of partial control in the synthesis of test cases from timed-automata specifications. We extend a previous approach to this problem from the untimed to the timed setting. This extension requires a deep reworking of the models, game interpretation and test-synthesis algorithms. We exhibit strategies of a game that try to minimize both cooperations of the system and distance to the satisfaction of a test purpose or to the next cooperation, and prove they are winning under some fairness assumptions. This entails that when turning those strategies into test cases, we get properties such as soundness and exhaustiveness of the test synthesis method. We finally propose a symbolic algorithm to compute those strategies.

@article{fmsd60(2)-HJM,
  author =              {Henry, L{\'e}o and J{\'e}ron, Thierry and Markey,
                         Nicolas},
  title =               {Control strategies for off-line testing of timed
                         systems},
  publisher =           {Springer-Verlag},
  journal =             {Formal Methods in System Design},
  volume =              {60},
  number =              {2},
  pages =               {147-194},
  year =                {2022},
  month =               apr,
  doi =                 {10.1007/s10703-022-00403-w},
  abstract =            {Partial observability and controllability are two
                         well-known issues in test-case synthesis for
                         reactive systems. We address the problem of partial
                         control in the synthesis of test cases from
                         timed-automata specifications. We extend a previous
                         approach to this problem from the untimed to the
                         timed setting. This extension requires a deep
                         reworking of the models, game interpretation and
                         test-synthesis algorithms. We exhibit strategies of
                         a game that try to minimize both cooperations of the
                         system and distance to the satisfaction of a test
                         purpose or to the next cooperation, and prove they
                         are winning under some fairness assumptions. This
                         entails that when turning those strategies into test
                         cases, we get properties such as soundness and
                         exhaustiveness of the test synthesis method. We
                         finally propose a symbolic algorithm to compute
                         those strategies.},
}
[HMR22] Loïc Hélouët, Nicolas Markey, and Ritam Raha. Reachability games with relaxed energy constraints. Information and Computation 285 (Part B). Elsevier, May 2022.
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 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, i.e., when the upper bound is reached, the extra energy is not 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 NP in the two-player setting. Allowing for bounded violations makes the problem PSPACE-complete for one-player arenas and EXPTIME-complete for two players. We then address the problem of existence of bounds for a given arena. We show that with reachability objectives, existence can be a simpler problem than the game itself, and conversely that with infinite games, existence can be harder.

@article{icomp2022-HMR,
  author =              {H{\'e}lou{\"e}t, Lo{\"\i}c and Markey, Nicolas and
                         Raha, Ritam},
  title =               {Reachability games with relaxed energy constraints},
  publisher =           {Elsevier},
  journal =             {Information and Computation},
  volume =              {285~(Part~B)},
  year =                {2022},
  month =               may,
  doi =                 {10.1016/j.ic.2021.104806},
  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 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, i.e.,
                         when the upper bound is reached, the extra energy is
                         not 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.
                         \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 NP in
                         the two-player setting. Allowing for bounded
                         violations makes the problem PSPACE-complete for
                         one-player arenas and EXPTIME-complete for two
                         players. We then address the problem of existence of
                         bounds for a given arena. We show that with
                         reachability objectives, existence can be a simpler
                         problem than the game itself, and conversely that
                         with infinite games, existence can be harder.},
}
[BMS+22] Nathalie Bertrand, Nicolas Markey, Suman Sadhukhan, and Ocan Sankur. Semilinear Representations for Series-Parallel Atomic Congestion Games. In FSTTCS'22, Leibniz International Proceedings in Informatics 250, pages 32:1-32:20. Leibniz-Zentrum für Informatik, December 2022.
Abstract

We consider atomic congestion games on series-parallel networks, and study the structure of the sets of Nash equilibria and social local optima on a given network when the number of players varies. We establish that these sets are definable in Presburger arithmetic and that they admit semilinear representations whose all period vectors have a common direction. As an application, we prove that the prices of anarchy and stability converge to 1 as the number of players goes to infinity, and show how to exploit these semilinear representations to compute these ratios precisely for a given network and number of players.

@inproceedings{fsttcs2022-BMSS,
  author =              {Bertrand, Nathalie and Markey, Nicolas and
                         Sadhukhan, Suman and Sankur, Ocan},
  title =               {Semilinear Representations for Series-Parallel
                         Atomic Congestion Games},
  editor =              {Dawar, Anuj and Guruswami, Venkatesan},
  booktitle =           {{P}roceedings of the 42nd {C}onference on
                         {F}oundations of {S}oftware {T}echnology and
                         {T}heoretical {C}omputer {S}cience ({FSTTCS}'22)},
  acronym =             {{FSTTCS}'22},
  publisher =           {Leibniz-Zentrum f{\"u}r Informatik},
  series =              {Leibniz International Proceedings in Informatics},
  volume =              {250},
  pages =               {32:1-32:20},
  year =                {2022},
  month =               dec,
  doi =                 {10.4230/LIPIcs.FSTTCS.2022.32},
  abstract =            {We~consider atomic congestion games on
                         series-parallel networks, and study the structure of
                         the sets of Nash equilibria and social local optima
                         on a given network when the number of players
                         varies. We establish that these sets are definable
                         in Presburger arithmetic and that they admit
                         semilinear representations whose all period vectors
                         have a common direction. As~an~application, we~prove
                         that the prices of anarchy and stability converge
                         to~1 as the number of players goes to infinity, and
                         show how to exploit these semilinear representations
                         to compute these ratios precisely for a given
                         network and number of players.},
}
[BMS+22] Nathalie Bertrand, Nicolas Markey, Ocan Sankur, and Nicolas Waldburger. Parameterized safety verification of round-based shared-memory systems. In ICALP'22, Leibniz International Proceedings in Informatics, pages 113:1-113:20. Leibniz-Zentrum für Informatik, July 2022.
Abstract

We consider the parameterized verification problem for distributed algorithms where the goal is to develop techniques to prove the correctness of a given algorithm regardless of the number of participating processes. Motivated by an asynchronous binary consensus algorithm of [J. Aspnes; Fast deterministic consensus in a noisy environment; J. Algorithms, 2002], we consider round-based distributed algorithms communicating with shared memory. A particular challenge in these systems is that 1) the number of processes is unbounded, and, more importantly, 2) there is a fresh set of registers at each round. A verification algorithm thus needs to manage both sources of infinity. In this setting, we prove that the safety verification problem, which consists in deciding whether all possible executions avoid a given error state, is PSPACE-complete. For negative instances of the safety verification problem, we also provide exponential lower and upper bounds on the minimal number of processes needed for an error execution and on the minimal round on which the error state can be covered.

@inproceedings{icalp2022-BMSW,
  author =              {Bertrand, Nathalie and Markey, Nicolas and Sankur,
                         Ocan and Waldburger, Nicolas},
  title =               {Parameterized safety verification of round-based
                         shared-memory systems},
  editor =              {Woodruff, David and Boja{\'n}czyk, Miko{\l}aj},
  booktitle =           {{P}roceedings of the 49th {I}nternational
                         {C}olloquium on {A}utomata, {L}anguages and
                         {P}rogramming ({ICALP}'22)},
  acronym =             {{ICALP}'22},
  publisher =           {Leibniz-Zentrum f{\"u}r Informatik},
  series =              {Leibniz International Proceedings in Informatics},
  pages =               {113:1-113:20},
  year =                {2022},
  month =               jul,
  doi =                 {10.4230/LIPIcs.ICALP.2022.113},
  abstract =            {We consider the parameterized verification problem
                         for distributed algorithms where the goal is to
                         develop techniques to prove the correctness of a
                         given algorithm regardless of the number of
                         participating processes. Motivated by an
                         asynchronous binary consensus algorithm~of
                         [J.~Aspnes; Fast deterministic consensus in a noisy
                         environment; J.~Algorithms,~2002], we~consider
                         round-based distributed algorithms communicating
                         with shared memory. A~particular challenge in these
                         systems is that 1)~the~number of processes is
                         unbounded, and, more importantly, 2)~there is a
                         fresh set of registers at each round. A~verification
                         algorithm thus needs to manage both sources of
                         infinity. In~this setting, we~prove that the safety
                         verification problem, which consists in deciding
                         whether all possible executions avoid a given error
                         state, is PSPACE-complete. For~negative instances of
                         the safety verification problem, we~also provide
                         exponential lower and upper bounds on the minimal
                         number of processes needed for an error execution
                         and on the minimal round on which the error state
                         can be covered.},
}
[GM22] Thomas Guyet and Nicolas Markey. Logical forms of chronicles. In TIME'22, Leibniz International Proceedings in Informatics, pages 7:1-7:15. Leibniz-Zentrum für Informatik, November 2022.
Abstract

A chronicle is a temporal model introduced by Dousson et al. for situation recognition. In short, a chronicle consists of a set of events and a set of real-valued temporal constraints on the delays between pairs of events. This work investigates the relationship between chronicles and classical temporal model formalisms, namely TPTL and MTL. More specifically, we answer the following question: is it possible to find an equivalent formula in such formalisms for any chronicle? This question arises from the observation that a single chronicle captures complex temporal behaviours that do not order the events in time.

In this article, we introduce the subclass of linear chronicles, which defines a temporal order of occurrence of the event to be recognized in a temporal sequence. Our first result is that any chronicle can be expressed as a disjunction of linear chronicles. Our second result is that any linear chronicle has an equivalent TPTL formula. Using existing expressiveness results between TPTL and MTL, we show that some chronicles have no equivalent in MTL. This confirms that the model of chronicle has interesting properties for situation recognition.

@inproceedings{time2022-GM,
  author =              {Guyet, {\relax Th}omas and Markey, Nicolas},
  title =               {Logical forms of chronicles},
  editor =              {Artikis, Alexander and Posenato, Roberto and
                         Tonetta, Stefano},
  booktitle =           {{P}roceedings of the 29th {I}nternational
                         {S}ymposium on {T}emporal {R}epresentation and
                         {R}easoning ({TIME}'22)},
  acronym =             {{TIME}'22},
  publisher =           {Leibniz-Zentrum f{\"u}r Informatik},
  series =              {Leibniz International Proceedings in Informatics},
  pages =               {7:1-7:15},
  year =                {2022},
  month =               nov,
  doi =                 {10.4230/LIPIcs.TIME.2022.7},
  abstract =            {A~chronicle is a temporal model introduced by
                         Dousson~\textit{et~al.} for situation recognition.
                         In~short, a chronicle consists of a set of events
                         and a set of real-valued temporal constraints on the
                         delays between pairs of events. This~work
                         investigates the relationship between chronicles and
                         classical temporal model formalisms, namely
                         \textsf{TPTL} and~\textsf{MTL}. More~specifically,
                         we~answer the following question: is~it possible to
                         find an equivalent formula in such formalisms for
                         any chronicle? This~question arises from the
                         observation that a single chronicle captures complex
                         temporal behaviours that do not order the events in
                         time.\par In~this article, we~introduce the subclass
                         of linear chronicles, which defines a temporal order
                         of occurrence of the event to be recognized in a
                         temporal sequence. Our~first result is that any
                         chronicle can be expressed as a disjunction of
                         linear chronicles. Our~second result is that any
                         linear chronicle has an equivalent \textsf{TPTL}
                         formula. Using existing expressiveness results
                         between \textsf{TPTL} and~\textsf{MTL}, we~show that
                         some chronicles have no equivalent in~\textsf{MTL}.
                         This confirms that the model of chronicle has
                         interesting properties for situation recognition.},
}
[GMS22] Aline Goeminne, Nicolas Markey, and Ocan Sankur. Non-Blind Strategies in Timed Network Congestion Games. In FORMATS'22, Lecture Notes in Computer Science 13465, pages 183-199. Springer-Verlag, September 2022.
Abstract

Network congestion games are a convenient model for reasoning about routing problems in a network: agents have to move from a source to a target vertex while avoiding congestion, measured as a cost depending on the number of players using the same link. Network congestion games have been extensively studied over the last 40 years, while their extension with timing constraints were considered more recently.

Most of the results on network congestion games consider blind strategies: they are static, and do not adapt to the strategies selected by the other players. We extend the recent results of [Bertrand et al., Dynamic network congestion games. FSTTCS'20] to timed network congestion games, in which the availability of the edges depend on (discrete) time. We prove that computing Nash equilibria satisfying some constraint on the total cost (and in particular, computing the best and worst Nash equilibria), and computing the social optimum, can be achieved in exponential space. The social optimum can be computed in polynomial space if all players have the same source and target.

@inproceedings{formats2022-GMS,
  author =              {Goeminne, Aline and Markey, Nicolas and Sankur,
                         Ocan},
  title =               {Non-Blind Strategies in Timed Network Congestion
                         Games},
  editor =              {Bogomolov, Sergiy and Parker, David},
  booktitle =           {{P}roceedings of the 20th {I}nternational
                         {C}onferences on {F}ormal {M}odelling and {A}nalysis
                         of {T}imed {S}ystems ({FORMATS}'22)},
  acronym =             {{FORMATS}'22},
  publisher =           {Springer-Verlag},
  series =              {Lecture Notes in Computer Science},
  volume =              {13465},
  pages =               {183-199},
  year =                {2022},
  month =               sep,
  doi =                 {10.1007/978-3-031-15839-1_11},
  abstract =            {Network congestion games are a convenient model for
                         reasoning about routing problems in a network:
                         agents have to move from a source to a target vertex
                         while avoiding congestion, measured as a cost
                         depending on the number of players using the same
                         link. Network congestion games have been extensively
                         studied over the last 40 years, while their
                         extension with timing constraints were considered
                         more recently. \par Most of the results on network
                         congestion games consider blind strategies: they are
                         static, and do not adapt to the strategies selected
                         by the other players. We extend the recent results
                         of [Bertrand~\textit{et~al.}, Dynamic network
                         congestion games. FSTTCS'20] to timed network
                         congestion games, in which the availability of the
                         edges depend on (discrete) time. We prove that
                         computing Nash equilibria satisfying some constraint
                         on the total cost (and in particular, computing the
                         best and worst Nash equilibria), and computing the
                         social optimum, can be achieved in exponential
                         space. The social optimum can be computed in
                         polynomial space if all players have the same source
                         and target.},
}
[NSJ+22] Reiya Noguchi, Ocan Sankur, Thierry Jéron, Nicolas Markey, and David Mentré. Repairing Real-Time Requirements. In ATVA'22, Lecture Notes in Computer Science 13505, pages 371-387. Springer-Verlag, October 2022.
Abstract

We consider the problem of repairing inconsistent real-time requirements with respect to two consistency notions: non-vacuity, which means that each requirement can be realized without violating other ones, and rt-consistency, which means that inevitable violations are detected immediately. We provide an iterative algorithm, based on solving SMT queries, to replace designated parameters of real-time requirements with new Boolean expressions and time constraints, so that the resulting set of requirements becomes consistent.

@inproceedings{atva2022-NSJMM,
  author =              {Noguchi, Reiya and Sankur, Ocan and J{\'e}ron,
                         Thierry and Markey, Nicolas and Mentr{\'e}, David},
  title =               {Repairing Real-Time Requirements},
  editor =              {Bouajjani, Ahmed and Hol{\'\i}k, Luk{\'a}{\v s} and
                         Wu, Zhilin},
  booktitle =           {{P}roceedings of the 20th {I}nternational
                         {S}ymposium on {A}utomated {T}echnology for
                         {V}erification and {A}nalysis ({ATVA}'22)},
  acronym =             {{ATVA}'22},
  publisher =           {Springer-Verlag},
  series =              {Lecture Notes in Computer Science},
  volume =              {13505},
  pages =               {371-387},
  year =                {2022},
  month =               oct,
  doi =                 {10.1007/978-3-031-19992-9_24},
  abstract =            {We~consider the problem of repairing inconsistent
                         real-time requirements with respect to two
                         consistency notions: non-vacuity, which means that
                         each requirement can be realized without violating
                         other ones, and rt-consistency, which means that
                         inevitable violations are detected immediately.
                         We~provide an iterative algorithm, based on solving
                         SMT queries, to replace designated parameters of
                         real-time requirements with new Boolean expressions
                         and time constraints, so that the resulting set of
                         requirements becomes consistent.},
}
[NJM+22] Reiya Noguchi, Thierry Jéron, Nicolas Markey, and Ocan Sankur. Method and system for testing the operation of a target computer system by using timed requirements. Patent EP 3 907 615 B1, November 2022, 
@patent{EP3907615B1,
  author =              {Noguchi, Reiya and J{\'e}ron, Thierry and Markey,
                         Nicolas and Sankur, Ocan},
  title =               {Method and system for testing the operation of a
                         target computer system by using timed requirements},
  number =              {EP 3 907 615 B1},
  year =                {2022},
  month =               nov,
}
[BHL+22] Sougata Bose, Thomas A. Henzinger, Karoliina Lehtinen, Sven Schewe, and Patrick Totzke. History-deterministic timed automata are not determinizable. In RP'22, Lecture Notes in Computer Science 13608, pages 67-76. Springer-Verlag, October 2022. 
@inproceedings{rp2022-BHLST,
  author =              {Bose, Sougata and Henzinger, Thomas A. and Lehtinen,
                         Karoliina and Schewe, Sven and Totzke, Patrick},
  title =               {History-deterministic timed automata are not
                         determinizable},
  editor =              {Lin, Anthony W. and Zetzsche, Georg and Potapov,
                         Igor},
  booktitle =           {{P}roceedings of the 16th {W}orkshop on
                         {R}eachability {P}roblems in {C}omputational
                         {M}odels ({RP}'22)},
  acronym =             {{RP}'22},
  publisher =           {Springer-Verlag},
  series =              {Lecture Notes in Computer Science},
  volume =              {13608},
  pages =               {67-76},
  year =                {2022},
  month =               oct,
  doi =                 {10.1007/978-3-031-19135-0_5},
}
[BL22] Udi Boker and Karoliina Lehtinen. Token Games and History-Deterministic Quantitative Automata. In FoSSaCS'22, Lecture Notes in Computer Science 13242, pages 120-139. Springer-Verlag, April 2022. 
@inproceedings{fossacs2022-BL,
  author =              {Boker, Udi and Lehtinen, Karoliina},
  title =               {Token Games and History-Deterministic Quantitative
                         Automata},
  editor =              {Bouyer, Patricia and Schr{\"o}der, Lutz},
  booktitle =           {{P}roceedings of the 25th {I}nternational
                         {C}onference on {F}oundations of {S}oftware
                         {S}cience and {C}omputation {S}tructure
                         ({FoSSaCS}'22)},
  acronym =             {{FoSSaCS}'22},
  publisher =           {Springer-Verlag},
  series =              {Lecture Notes in Computer Science},
  volume =              {13242},
  pages =               {120-139},
  year =                {2022},
  month =               apr,
  doi =                 {10.1007/978-3-030-99253-8_7},
}
[BLS22] Udi Boker, Karoliina Lehtinen, and Salomon Sickert. On the Translation of Automata to Linear Temporal Logic. In FoSSaCS'22, Lecture Notes in Computer Science 13242, pages 140-160. Springer-Verlag, April 2022. 
@inproceedings{fossacs2022-BLS,
  author =              {Boker, Udi and Lehtinen, Karoliina and Sickert,
                         Salomon},
  title =               {On the Translation of Automata to Linear Temporal
                         Logic},
  editor =              {Bouyer, Patricia and Schr{\"o}der, Lutz},
  booktitle =           {{P}roceedings of the 25th {I}nternational
                         {C}onference on {F}oundations of {S}oftware
                         {S}cience and {C}omputation {S}tructure
                         ({FoSSaCS}'22)},
  acronym =             {{FoSSaCS}'22},
  publisher =           {Springer-Verlag},
  series =              {Lecture Notes in Computer Science},
  volume =              {13242},
  pages =               {140-160},
  year =                {2022},
  month =               apr,
  doi =                 {10.1007/978-3-030-99253-8_8},
}
[HLT22] Thomas A. Henzinger, Karoliina Lehtinen, and Patrick Totzke. History-deterministic timed automata. In CONCUR'22, Leibniz International Proceedings in Informatics 243, pages 14:1-14:21. Leibniz-Zentrum für Informatik, September 2022. 
@inproceedings{concur2022-HLT,
  author =              {Henzinger, Thomas A. and Lehtinen, Karoliina and
                         Totzke, Patrick},
  title =               {History-deterministic timed automata},
  editor =              {Klin, Bartek and Lasota, S{\l}awomir and Muscholl,
                         Anca},
  booktitle =           {{P}roceedings of the 33rd {I}nternational
                         {C}onference on {C}oncurrency {T}heory
                         ({CONCUR}'22)},
  acronym =             {{CONCUR}'22},
  publisher =           {Leibniz-Zentrum f{\"u}r Informatik},
  series =              {Leibniz International Proceedings in Informatics},
  volume =              {243},
  pages =               {14:1-14:21},
  year =                {2022},
  month =               sep,
  doi =                 {10.4230/LIPIcs.CONCUR.2022.14},
}
[HM22] Bainian Hao and Carla Michini. Inefficiency of Pure Nash Equilibria in Series-Parallel Network Congestion Games. In WINE'22, Lecture Notes in Computer Science 13778, pages 3-20. Springer-Verlag, July 2022. 
@inproceedings{wine2022-HM,
  author =              {Hao, Bainian and Michini, Carla},
  title =               {Inefficiency of Pure Nash Equilibria in
                         Series-Parallel Network Congestion Games},
  editor =              {Hansen, Kristoffer Arnsfelt and Liu, Tracy Xiao and
                         Malekian, Azarakhsh},
  booktitle =           {{P}roceedings of the 18th {I}nternational
                         {C}onference on {W}eb and {I}nternet {E}conomics
                         ({WINE}'22)},
  acronym =             {{WINE}'22},
  publisher =           {Springer-Verlag},
  series =              {Lecture Notes in Computer Science},
  volume =              {13778},
  pages =               {3-20},
  year =                {2022},
  month =               jul,
  doi =                 {10.1007/978-3-031-22832-2_1},
}
List of authors