2022 | |
---|---|

[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.
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}, year = {2022}, month = dec, 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.
Leibniz-Zentrum für Informatik, November 2022. To appear.
- 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 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}, year = {2022}, month = nov, note = {To~appear}, 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 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 TPTL and 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.
Springer-Verlag, October 2022. To appear.
- 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}, year = {2022}, month = oct, note = {To~appear}, 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.}, } |

[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, Jochen}, 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}, } |

- 2
- 1
- 1
- 1
- 1
- 1
- 1
- 1
- 1
- 1
- 1
- 4
- 1