2022 | |
---|---|

[HJM22] | Léo Henry,
Thierry Jéron et
Nicolas Markey.
Control strategies for off-line testing of timed
systems.
Formal Methods in System Design 60(2):147-194. Springer-Verlag, avril 2022.
- Résumé
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 et
Ritam Raha.
Reachability games with relaxed energy constraints.
Information and Computation 285 (Part B).
Elsevier, mai 2022.
- Résumé
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 et
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, décembre 2022.
- Résumé
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 et
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, juillet 2022.
- Résumé
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 et
Nicolas Markey.
Logical forms of chronicles.
In TIME'22,
Leibniz International Proceedings in Informatics, pages 7:1-7:15. Leibniz-Zentrum für Informatik, novembre 2022.
- Résumé
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 et
Ocan Sankur.
Non-Blind Strategies in Timed Network Congestion
Games.
In FORMATS'22,
Lecture Notes in Computer Science 13465, pages 183-199. Springer-Verlag, septembre 2022.
- Résumé
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 et
David Mentré.
Repairing Real-Time Requirements.
In ATVA'22,
Lecture Notes in Computer Science 13505, pages 371-387. Springer-Verlag, octobre 2022.
- Résumé
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 et
Ocan Sankur.
Method and system for testing the operation of a
target computer system by using timed requirements.
Brevet EP 3 907 615 B1, novembre 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 et
Patrick Totzke.
History-deterministic timed automata are not
determinizable.
In RP'22,
Lecture Notes in Computer Science 13608, pages 67-76. Springer-Verlag, octobre 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 et
Karoliina Lehtinen.
Token Games and History-Deterministic Quantitative
Automata.
In FoSSaCS'22,
Lecture Notes in Computer Science 13242, pages 120-139. Springer-Verlag, avril 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 et
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, avril 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 et
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, septembre 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 et
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, juillet 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}, } |

- 2
- 2
- 1
- 1
- 1
- 1
- 1
- 1
- 2
- 3
- 4
- 8
- 1
- 1
- 2
- 1
- 1
- 5
- 1
- 1
- 2
- 1