21 Search Results for "Markey, Nicolas"

Document
DOI: 10.4230/LIPIcs.MFCS.2023.88
Checking Presence Reachability Properties on Parameterized Shared-Memory Systems

Authors: Nicolas Waldburger

Published in: LIPIcs, Volume 272, 48th International Symposium on Mathematical Foundations of Computer Science (MFCS 2023)

Abstract
We consider the verification of distributed systems composed of an arbitrary number of asynchronous processes. Processes are identical finite-state machines that communicate by reading from and writing to a shared memory. Beyond the standard model with finitely many registers, we tackle round-based shared-memory systems with fresh registers at each round. In the latter model, both the number of processes and the number of registers are unbounded, making verification particularly challenging. The properties studied are generic presence reachability objectives, which subsume classical questions such as safety or synchronization by expressing the presence or absence of processes in some states. In the more general round-based setting, we establish that the parameterized verification of presence reachability properties is PSPACE-complete. Moreover, for the roundless model with finitely many registers, we prove that the complexity drops down to NP-complete and we provide several natural restrictions that make the problem solvable in polynomial time.
Cite as

Nicolas Waldburger. Checking Presence Reachability Properties on Parameterized Shared-Memory Systems. In 48th International Symposium on Mathematical Foundations of Computer Science (MFCS 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 272, pp. 88:1-88:15, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)

Copy BibTex To Clipboard

@InProceedings{waldburger:LIPIcs.MFCS.2023.88,
  author =	{Waldburger, Nicolas},
  title =	{{Checking Presence Reachability Properties on Parameterized Shared-Memory Systems}},
  booktitle =	{48th International Symposium on Mathematical Foundations of Computer Science (MFCS 2023)},
  pages =	{88:1--88:15},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-292-1},
  ISSN =	{1868-8969},
  year =	{2023},
  volume =	{272},
  editor =	{Leroux, J\'{e}r\^{o}me and Lombardy, Sylvain and Peleg, David},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.MFCS.2023.88},
  URN =		{urn:nbn:de:0030-drops-186225},
  doi =		{10.4230/LIPIcs.MFCS.2023.88},
  annote =	{Keywords: Verification, Parameterized models, Distributed algorithms}
}
Document
DOI: 10.4230/LIPIcs.FSTTCS.2022.32
Semilinear Representations for Series-Parallel Atomic Congestion Games

Authors: Nathalie Bertrand, Nicolas Markey, Suman Sadhukhan, and Ocan Sankur

Published in: LIPIcs, Volume 250, 42nd IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 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.
Cite as

Nathalie Bertrand, Nicolas Markey, Suman Sadhukhan, and Ocan Sankur. Semilinear Representations for Series-Parallel Atomic Congestion Games. In 42nd IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 250, pp. 32:1-32:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)

Copy BibTex To Clipboard

@InProceedings{bertrand_et_al:LIPIcs.FSTTCS.2022.32,
  author =	{Bertrand, Nathalie and Markey, Nicolas and Sadhukhan, Suman and Sankur, Ocan},
  title =	{{Semilinear Representations for Series-Parallel Atomic Congestion Games}},
  booktitle =	{42nd IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2022)},
  pages =	{32:1--32:20},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-261-7},
  ISSN =	{1868-8969},
  year =	{2022},
  volume =	{250},
  editor =	{Dawar, Anuj and Guruswami, Venkatesan},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.FSTTCS.2022.32},
  URN =		{urn:nbn:de:0030-drops-174243},
  doi =		{10.4230/LIPIcs.FSTTCS.2022.32},
  annote =	{Keywords: congestion games, Nash equilibria, Presburger arithmetic, semilinear sets, price of anarchy}
}
Document
DOI: 10.4230/LIPIcs.TIME.2022.7
Logical Forms of Chronicles

Authors: Thomas Guyet and Nicolas Markey

Published in: LIPIcs, Volume 247, 29th International Symposium on Temporal Representation and Reasoning (TIME 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, without imposing a particular order of the events in time. For our purpose, we introduce the subclass of linear chronicles, which set the order of occurrence of the events 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.
Cite as

Thomas Guyet and Nicolas Markey. Logical Forms of Chronicles. In 29th International Symposium on Temporal Representation and Reasoning (TIME 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 247, pp. 7:1-7:15, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)

Copy BibTex To Clipboard

@InProceedings{guyet_et_al:LIPIcs.TIME.2022.7,
  author =	{Guyet, Thomas and Markey, Nicolas},
  title =	{{Logical Forms of Chronicles}},
  booktitle =	{29th International Symposium on Temporal Representation and Reasoning (TIME 2022)},
  pages =	{7:1--7:15},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-262-4},
  ISSN =	{1868-8969},
  year =	{2022},
  volume =	{247},
  editor =	{Artikis, Alexander and Posenato, Roberto and Tonetta, Stefano},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.TIME.2022.7},
  URN =		{urn:nbn:de:0030-drops-172542},
  doi =		{10.4230/LIPIcs.TIME.2022.7},
  annote =	{Keywords: temporal logics, temporal models}
}
Document
Track B: Automata, Logic, Semantics, and Theory of Programming
DOI: 10.4230/LIPIcs.ICALP.2022.113
Parameterized Safety Verification of Round-Based Shared-Memory Systems

Authors: Nathalie Bertrand, Nicolas Markey, Ocan Sankur, and Nicolas Waldburger

Published in: LIPIcs, Volume 229, 49th International Colloquium on Automata, Languages, and Programming (ICALP 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 [James Aspnes, 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.
Cite as

Nathalie Bertrand, Nicolas Markey, Ocan Sankur, and Nicolas Waldburger. Parameterized Safety Verification of Round-Based Shared-Memory Systems. In 49th International Colloquium on Automata, Languages, and Programming (ICALP 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 229, pp. 113:1-113:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)

Copy BibTex To Clipboard

@InProceedings{bertrand_et_al:LIPIcs.ICALP.2022.113,
  author =	{Bertrand, Nathalie and Markey, Nicolas and Sankur, Ocan and Waldburger, Nicolas},
  title =	{{Parameterized Safety Verification of Round-Based Shared-Memory Systems}},
  booktitle =	{49th International Colloquium on Automata, Languages, and Programming (ICALP 2022)},
  pages =	{113:1--113:20},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-235-8},
  ISSN =	{1868-8969},
  year =	{2022},
  volume =	{229},
  editor =	{Boja\'{n}czyk, Miko{\l}aj and Merelli, Emanuela and Woodruff, David P.},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.ICALP.2022.113},
  URN =		{urn:nbn:de:0030-drops-164541},
  doi =		{10.4230/LIPIcs.ICALP.2022.113},
  annote =	{Keywords: Verification, Parameterized models, Distributed algorithms}
}
Document
DOI: 10.4230/LIPIcs.FSTTCS.2020.40
Dynamic Network Congestion Games

Authors: Nathalie Bertrand, Nicolas Markey, Suman Sadhukhan, and Ocan Sankur

Published in: LIPIcs, Volume 182, 40th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2020)

Abstract
Congestion games are a classical type of games studied in game theory, in which n players choose a resource, and their individual cost increases with the number of other players choosing the same resource. In network congestion games (NCGs), the resources correspond to simple paths in a graph, e.g. representing routing options from a source to a target. In this paper, we introduce a variant of NCGs, referred to as dynamic NCGs: in this setting, players take transitions synchronously, they select their next transitions dynamically, and they are charged a cost that depends on the number of players simultaneously using the same transition. We study, from a complexity perspective, standard concepts of game theory in dynamic NCGs: social optima, Nash equilibria, and subgame perfect equilibria. Our contributions are the following: the existence of a strategy profile with social cost bounded by a constant is in PSPACE and NP-hard. (Pure) Nash equilibria always exist in dynamic NCGs; the existence of a Nash equilibrium with bounded cost can be decided in EXPSPACE, and computing a witnessing strategy profile can be done in doubly-exponential time. The existence of a subgame perfect equilibrium with bounded cost can be decided in 2EXPSPACE, and a witnessing strategy profile can be computed in triply-exponential time.
Cite as

Nathalie Bertrand, Nicolas Markey, Suman Sadhukhan, and Ocan Sankur. Dynamic Network Congestion Games. In 40th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2020). Leibniz International Proceedings in Informatics (LIPIcs), Volume 182, pp. 40:1-40:16, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020)

Copy BibTex To Clipboard

@InProceedings{bertrand_et_al:LIPIcs.FSTTCS.2020.40,
  author =	{Bertrand, Nathalie and Markey, Nicolas and Sadhukhan, Suman and Sankur, Ocan},
  title =	{{Dynamic Network Congestion Games}},
  booktitle =	{40th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2020)},
  pages =	{40:1--40:16},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-174-0},
  ISSN =	{1868-8969},
  year =	{2020},
  volume =	{182},
  editor =	{Saxena, Nitin and Simon, Sunil},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.FSTTCS.2020.40},
  URN =		{urn:nbn:de:0030-drops-132811},
  doi =		{10.4230/LIPIcs.FSTTCS.2020.40},
  annote =	{Keywords: Congestion games, Nash equilibria, Subgame perfect equilibria, Complexity}
}
Document
Invited Talk
DOI: 10.4230/LIPIcs.TIME.2019.3
On the Computation of Nash Equilibria in Games on Graphs (Invited Talk)

Authors: Patricia Bouyer

Published in: LIPIcs, Volume 147, 26th International Symposium on Temporal Representation and Reasoning (TIME 2019)

Abstract
In this talk, I will show how one can characterize and compute Nash equilibria in multiplayer games played on graphs. I will present in particular a construction, called the suspect game construction, which allows to reduce the computation of Nash equilibria to the computation of winning strategies in a two-player zero-sum game.
Cite as

Patricia Bouyer. On the Computation of Nash Equilibria in Games on Graphs (Invited Talk). In 26th International Symposium on Temporal Representation and Reasoning (TIME 2019). Leibniz International Proceedings in Informatics (LIPIcs), Volume 147, pp. 3:1-3:3, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019)

Copy BibTex To Clipboard

@InProceedings{bouyer:LIPIcs.TIME.2019.3,
  author =	{Bouyer, Patricia},
  title =	{{On the Computation of Nash Equilibria in Games on Graphs}},
  booktitle =	{26th International Symposium on Temporal Representation and Reasoning (TIME 2019)},
  pages =	{3:1--3:3},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-127-6},
  ISSN =	{1868-8969},
  year =	{2019},
  volume =	{147},
  editor =	{Gamper, Johann and Pinchinat, Sophie and Sciavicco, Guido},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.TIME.2019.3},
  URN =		{urn:nbn:de:0030-drops-113616},
  doi =		{10.4230/LIPIcs.TIME.2019.3},
  annote =	{Keywords: Multiplayer games, Nash equilibria}
}
Document
DOI: 10.4230/LIPIcs.STACS.2018.34
Dependences in Strategy Logic

Authors: Patrick Gardy, Patricia Bouyer, and Nicolas Markey

Published in: LIPIcs, Volume 96, 35th Symposium on Theoretical Aspects of Computer Science (STACS 2018)

Abstract
Strategy Logic (SL) is a very expressive temporal logic for specifying and verifying properties of multi-agent systems: in SL, one can quantify over strategies, assign them to agents, and express LTL properties of the resulting plays. Such a powerful framework has two drawbacks: First, model checking SL has non-elementary complexity; second, the exact semantics of SL is rather intricate, and may not correspond to what is expected. In this paper, we focus on strategy dependences in SL, by tracking how existentially-quantified strategies in a formula may (or may not) depend on other strategies selected in the formula, revisiting the approach of [Mogavero et al., Reasoning about strategies: On the model-checking problem, 2014]. We explain why elementary dependences, as defined by Mogavero et al., do not exactly capture the intended concept of behavioral strategies. We address this discrepancy by introducing timeline dependences, and exhibit a large fragment of SL for which model checking can be performed in 2-EXPTIME under this new semantics.
Cite as

Patrick Gardy, Patricia Bouyer, and Nicolas Markey. Dependences in Strategy Logic. In 35th Symposium on Theoretical Aspects of Computer Science (STACS 2018). Leibniz International Proceedings in Informatics (LIPIcs), Volume 96, pp. 34:1-34:15, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2018)

Copy BibTex To Clipboard

@InProceedings{gardy_et_al:LIPIcs.STACS.2018.34,
  author =	{Gardy, Patrick and Bouyer, Patricia and Markey, Nicolas},
  title =	{{Dependences in Strategy Logic}},
  booktitle =	{35th Symposium on Theoretical Aspects of Computer Science (STACS 2018)},
  pages =	{34:1--34:15},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-062-0},
  ISSN =	{1868-8969},
  year =	{2018},
  volume =	{96},
  editor =	{Niedermeier, Rolf and Vall\'{e}e, Brigitte},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.STACS.2018.34},
  URN =		{urn:nbn:de:0030-drops-85320},
  doi =		{10.4230/LIPIcs.STACS.2018.34},
  annote =	{Keywords: strategic reasoning, strategy logic, dependences, behavioural strategies.}
}
Document
Invited Talk
DOI: 10.4230/LIPIcs.MFCS.2017.84
Temporal Logics for Multi-Agent Systems (Invited Talk)

Authors: Nicolas Markey

Published in: LIPIcs, Volume 83, 42nd International Symposium on Mathematical Foundations of Computer Science (MFCS 2017)

Abstract
This is an overview of an invited talk delivered during the 42nd International Conference on Mathematical Foundations of Computer Science (MFCS 2017).
Cite as

Nicolas Markey. Temporal Logics for Multi-Agent Systems (Invited Talk). In 42nd International Symposium on Mathematical Foundations of Computer Science (MFCS 2017). Leibniz International Proceedings in Informatics (LIPIcs), Volume 83, pp. 84:1-84:3, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2017)

Copy BibTex To Clipboard

@InProceedings{markey:LIPIcs.MFCS.2017.84,
  author =	{Markey, Nicolas},
  title =	{{Temporal Logics for Multi-Agent Systems}},
  booktitle =	{42nd International Symposium on Mathematical Foundations of Computer Science (MFCS 2017)},
  pages =	{84:1--84:3},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-046-0},
  ISSN =	{1868-8969},
  year =	{2017},
  volume =	{83},
  editor =	{Larsen, Kim G. and Bodlaender, Hans L. and Raskin, Jean-Francois},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.MFCS.2017.84},
  URN =		{urn:nbn:de:0030-drops-81368},
  doi =		{10.4230/LIPIcs.MFCS.2017.84},
  annote =	{Keywords: Temporal logics, verification, game theory, strategic reasoning.}
}
Document
DOI: 10.4230/LIPIcs.CONCUR.2016.28
On the Expressiveness of QCTL

Authors: Amélie David, Francois Laroussinie, and Nicolas Markey

Published in: LIPIcs, Volume 59, 27th International Conference on Concurrency Theory (CONCUR 2016)

Abstract
QCTL extends the temporal logic CTL with quantification over atomic propositions. While the algorithmic questions for QCTL and its fragments with limited quantification depth are well-understood (e.g. satisfiability of QkCTL, with at most k nested blocks of quantifiers, is (k+1)-EXPTIME-complete), very few results are known about the expressiveness of this logic. We address such expressiveness questions in this paper. We first consider the distinguishing power of these logics (i.e., their ability to separate models), their relationship with behavioural equivalences, and their ability to capture the behaviours of finite Kripke structures with so-called characteristic formulas. We then consider their expressive power (i.e., their ability to express a property), showing that in terms of expressiveness the hierarchy QkCTL collapses at level 2 (in other terms, any QCTL formula can be expressed using at most two nested blocks of quantifiers).
Cite as

Amélie David, Francois Laroussinie, and Nicolas Markey. On the Expressiveness of QCTL. In 27th International Conference on Concurrency Theory (CONCUR 2016). Leibniz International Proceedings in Informatics (LIPIcs), Volume 59, pp. 28:1-28:15, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2016)

Copy BibTex To Clipboard

@InProceedings{david_et_al:LIPIcs.CONCUR.2016.28,
  author =	{David, Am\'{e}lie and Laroussinie, Francois and Markey, Nicolas},
  title =	{{On the Expressiveness of QCTL}},
  booktitle =	{27th International Conference on Concurrency Theory (CONCUR 2016)},
  pages =	{28:1--28:15},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-017-0},
  ISSN =	{1868-8969},
  year =	{2016},
  volume =	{59},
  editor =	{Desharnais, Jos\'{e}e and Jagadeesan, Radha},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2016.28},
  URN =		{urn:nbn:de:0030-drops-61643},
  doi =		{10.4230/LIPIcs.CONCUR.2016.28},
  annote =	{Keywords: Specification, Verification, Temporal Logic, Expressiveness, Tree automata}
}
Document
DOI: 10.4230/LIPIcs.ICALP.2016.106
Reachability in Networks of Register Protocols under Stochastic Schedulers

Authors: Patricia Bouyer, Nicolas Markey, Mickael Randour, Arnaud Sangnier, and Daniel Stan

Published in: LIPIcs, Volume 55, 43rd International Colloquium on Automata, Languages, and Programming (ICALP 2016)

Abstract
We study the almost-sure reachability problem in a distributed system obtained as the asynchronous composition of N copies (called processes) of the same automaton (called protocol), that can communicate via a shared register with finite domain. The automaton has two types of transitions: write-transitions update the value of the register, while read-transitions move to a new state depending on the content of the register. Non-determinism is resolved by a stochastic scheduler. Given a protocol, we focus on almost-sure reachability of a target state by one of the processes. The answer to this problem naturally depends on the number N of processes. However, we prove that our setting has a cut-off property: the answer to the almost-sure reachability problem is constant when N is large enough; we then develop an EXPSPACE algorithm deciding whether this constant answer is positive or negative.
Cite as

Patricia Bouyer, Nicolas Markey, Mickael Randour, Arnaud Sangnier, and Daniel Stan. Reachability in Networks of Register Protocols under Stochastic Schedulers. In 43rd International Colloquium on Automata, Languages, and Programming (ICALP 2016). Leibniz International Proceedings in Informatics (LIPIcs), Volume 55, pp. 106:1-106:14, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2016)

Copy BibTex To Clipboard

@InProceedings{bouyer_et_al:LIPIcs.ICALP.2016.106,
  author =	{Bouyer, Patricia and Markey, Nicolas and Randour, Mickael and Sangnier, Arnaud and Stan, Daniel},
  title =	{{Reachability in Networks of Register Protocols under Stochastic Schedulers}},
  booktitle =	{43rd International Colloquium on Automata, Languages, and Programming (ICALP 2016)},
  pages =	{106:1--106:14},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-013-2},
  ISSN =	{1868-8969},
  year =	{2016},
  volume =	{55},
  editor =	{Chatzigiannakis, Ioannis and Mitzenmacher, Michael and Rabani, Yuval and Sangiorgi, Davide},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.ICALP.2016.106},
  URN =		{urn:nbn:de:0030-drops-62416},
  doi =		{10.4230/LIPIcs.ICALP.2016.106},
  annote =	{Keywords: Networks of Processes, Parametrized Systems, Stochastic Scheduler, Almost-sure Reachability, Cut-Off Property}
}
Document
DOI: 10.4230/LIPIcs.FSTTCS.2015.69
Weighted Strategy Logic with Boolean Goals Over One-Counter Games

Authors: Patricia Bouyer, Patrick Gardy, and Nicolas Markey

Published in: LIPIcs, Volume 45, 35th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2015)

Abstract
Strategy Logic is a powerful specification language for expressing non-zero-sum properties of multi-player games. SL conveniently extends the logic ATL with explicit quantification and assignment of strategies. In this paper, we consider games over one-counter automata, and a quantitative extension 1cSL of SL with assertions over the value of the counter. We prove two results: we first show that, if decidable, model checking the so-called Boolean-goal fragment of 1cSL has non-elementary complexity; we actually prove the result for the Boolean-goal fragment of SL over finite-state games, which was an open question in [Mogavero et al. Reasoning about strategies: On the model-checking problem. ACM ToCL 15(4),2014]. As a first step towards proving decidability, we then show that the Boolean-goal fragment of 1cSL over one-counter games enjoys a nice periodicity property.
Cite as

Patricia Bouyer, Patrick Gardy, and Nicolas Markey. Weighted Strategy Logic with Boolean Goals Over One-Counter Games. In 35th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2015). Leibniz International Proceedings in Informatics (LIPIcs), Volume 45, pp. 69-83, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2015)

Copy BibTex To Clipboard

@InProceedings{bouyer_et_al:LIPIcs.FSTTCS.2015.69,
  author =	{Bouyer, Patricia and Gardy, Patrick and Markey, Nicolas},
  title =	{{Weighted Strategy Logic with Boolean Goals Over One-Counter Games}},
  booktitle =	{35th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2015)},
  pages =	{69--83},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-97-2},
  ISSN =	{1868-8969},
  year =	{2015},
  volume =	{45},
  editor =	{Harsha, Prahladh and Ramalingam, G.},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.FSTTCS.2015.69},
  URN =		{urn:nbn:de:0030-drops-56537},
  doi =		{10.4230/LIPIcs.FSTTCS.2015.69},
  annote =	{Keywords: Temporal logics, multi-player games, strategy logic, quantitative games}
}
Document
DOI: 10.4230/OASIcs.SynCoP.2015.48
Game-based Synthesis of Distributed Controllers for Sampled Switched Systems

Authors: Laurent Fribourg, Ulrich Kühne, and Nicolas Markey

Published in: OASIcs, Volume 44, 2nd International Workshop on Synthesis of Complex Parameters (SynCoP'15) (2015)

Abstract
Switched systems are a convenient formalism for modeling physical processes interacting with a digital controller. Unfortunately, the formalism does not capture the distributed nature encountered e.g. in cyber-physical systems, which are organized as networks of elements interacting with local controllers. Most current methods for control synthesis can only produce a centralized controller, which is assumed to have complete knowledge of all the component states and can interact with all of them. In this paper, we consider a centralized-controller synthesis technique based on state-space decomposition, and use a game-based approach to extend it to a distributed framework.
Cite as

Laurent Fribourg, Ulrich Kühne, and Nicolas Markey. Game-based Synthesis of Distributed Controllers for Sampled Switched Systems. In 2nd International Workshop on Synthesis of Complex Parameters (SynCoP'15). Open Access Series in Informatics (OASIcs), Volume 44, pp. 48-62, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2015)

Copy BibTex To Clipboard

@InProceedings{fribourg_et_al:OASIcs.SynCoP.2015.48,
  author =	{Fribourg, Laurent and K\"{u}hne, Ulrich and Markey, Nicolas},
  title =	{{Game-based Synthesis of Distributed Controllers for Sampled Switched Systems}},
  booktitle =	{2nd International Workshop on Synthesis of Complex Parameters (SynCoP'15)},
  pages =	{48--62},
  series =	{Open Access Series in Informatics (OASIcs)},
  ISBN =	{978-3-939897-82-8},
  ISSN =	{2190-6807},
  year =	{2015},
  volume =	{44},
  editor =	{Andr\'{e}, \'{E}tienne and Frehse, Goran},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/OASIcs.SynCoP.2015.48},
  URN =		{urn:nbn:de:0030-drops-56091},
  doi =		{10.4230/OASIcs.SynCoP.2015.48},
  annote =	{Keywords: Cyber-physical systems, controller synthesis, games, robustness, partial observation}
}
Document
DOI: 10.4230/LIPIcs.CONCUR.2015.311
On the Value Problem in Weighted Timed Games

Authors: Patricia Bouyer, Samy Jaziri, and Nicolas Markey

Published in: LIPIcs, Volume 42, 26th International Conference on Concurrency Theory (CONCUR 2015)

Abstract
A weighted timed game is a timed game with extra quantitative information representing e.g. energy consumption. Optimizing the weight for reaching a target is a natural question, which has already been investigated for ten years. Existence of optimal strategies is known to be undecidable in general, and only very restricted classes of games have been identified for which optimal weight and almost-optimal strategies can be computed. In this paper, we show that the value problem is undecidable in weighted timed games. We then introduce a large subclass of weighted timed games (for which the undecidability proof above applies), and provide an algorithm to compute arbitrary approximations of the value in such games. To the best of our knowledge, this is the first approximation scheme for an undecidable class of weighted timed games.
Cite as

Patricia Bouyer, Samy Jaziri, and Nicolas Markey. On the Value Problem in Weighted Timed Games. In 26th International Conference on Concurrency Theory (CONCUR 2015). Leibniz International Proceedings in Informatics (LIPIcs), Volume 42, pp. 311-324, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2015)

Copy BibTex To Clipboard

@InProceedings{bouyer_et_al:LIPIcs.CONCUR.2015.311,
  author =	{Bouyer, Patricia and Jaziri, Samy and Markey, Nicolas},
  title =	{{On the Value Problem in Weighted Timed Games}},
  booktitle =	{26th International Conference on Concurrency Theory (CONCUR 2015)},
  pages =	{311--324},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-91-0},
  ISSN =	{1868-8969},
  year =	{2015},
  volume =	{42},
  editor =	{Aceto, Luca and de Frutos Escrig, David},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2015.311},
  URN =		{urn:nbn:de:0030-drops-53863},
  doi =		{10.4230/LIPIcs.CONCUR.2015.311},
  annote =	{Keywords: Timed games, undecidability, approximation}
}
Document
DOI: 10.4230/DagRep.5.2.1
Non-Zero-Sum-Games and Control (Dagstuhl Seminar 15061)

Authors: Krishnendu Chatterjee, Stéphane Lafortune, Nicolas Markey, and Wolfgang Thomas

Published in: Dagstuhl Reports, Volume 5, Issue 2 (2015)

Abstract
In this report, the program, research issues, and results of Dagstuhl Seminar 15061 "Non-Zero-Sum-Games and Control" are described. The area of non-zero-sum games is addressed in a wide range of topics: multi-player games, partial-observation games, quantitative game models, and - as a special focus - connections with control engineering (supervisory control).
Cite as

Krishnendu Chatterjee, Stéphane Lafortune, Nicolas Markey, and Wolfgang Thomas. Non-Zero-Sum-Games and Control (Dagstuhl Seminar 15061). In Dagstuhl Reports, Volume 5, Issue 2, pp. 1-25, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2015)

Copy BibTex To Clipboard

@Article{chatterjee_et_al:DagRep.5.2.1,
  author =	{Chatterjee, Krishnendu and Lafortune, St\'{e}phane and Markey, Nicolas and Thomas, Wolfgang},
  title =	{{Non-Zero-Sum-Games and Control (Dagstuhl Seminar 15061)}},
  pages =	{1--25},
  journal =	{Dagstuhl Reports},
  ISSN =	{2192-5283},
  year =	{2015},
  volume =	{5},
  number =	{2},
  editor =	{Chatterjee, Krishnendu and Lafortune, St\'{e}phane and Markey, Nicolas and Thomas, Wolfgang},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/DagRep.5.2.1},
  URN =		{urn:nbn:de:0030-drops-50424},
  doi =		{10.4230/DagRep.5.2.1},
  annote =	{Keywords: non-zero-sum games, infinite games, multi-player games, partial-observation games, quantitative games, controller synthesis, supervisory control}
}
Document
DOI: 10.4230/LIPIcs.FSTTCS.2014.121
Synchronizing Words for Weighted and Timed Automata

Authors: Laurent Doyen, Line Juhl, Kim G. Larsen, Nicolas Markey, and Mahsa Shirmohammadi

Published in: LIPIcs, Volume 29, 34th International Conference on Foundation of Software Technology and Theoretical Computer Science (FSTTCS 2014)

Abstract
The problem of synchronizing automata is concerned with the existence of a word that sends all states of the automaton to one and the same state. This problem has classically been studied for complete deterministic finite automata, with the existence problem being NLOGSPACE-complete. In this paper we consider synchronizing-word problems for weighted and timed automata. We consider the synchronization problem in several variants and combinations of these, including deterministic and non-deterministic timed and weighted automata, synchronization to unique location with possibly different clock valuations or accumulated weights, as well as synchronization with a safety condition forbidding the automaton to visit states outside a safety-set during synchronization (e.g. energy constraints). For deterministic weighted automata, the synchronization problem is proven PSPACE-complete under energy constraints, and in 3-EXPSPACE under general safety constraints. For timed automata the synchronization problems are shown to be PSPACE-complete in the deterministic case, and undecidable in the non-deterministic case.
Cite as

Laurent Doyen, Line Juhl, Kim G. Larsen, Nicolas Markey, and Mahsa Shirmohammadi. Synchronizing Words for Weighted and Timed Automata. In 34th International Conference on Foundation of Software Technology and Theoretical Computer Science (FSTTCS 2014). Leibniz International Proceedings in Informatics (LIPIcs), Volume 29, pp. 121-132, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2014)

Copy BibTex To Clipboard

@InProceedings{doyen_et_al:LIPIcs.FSTTCS.2014.121,
  author =	{Doyen, Laurent and Juhl, Line and Larsen, Kim G. and Markey, Nicolas and Shirmohammadi, Mahsa},
  title =	{{Synchronizing Words for Weighted and Timed Automata}},
  booktitle =	{34th International Conference on Foundation of Software Technology and Theoretical Computer Science (FSTTCS 2014)},
  pages =	{121--132},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-77-4},
  ISSN =	{1868-8969},
  year =	{2014},
  volume =	{29},
  editor =	{Raman, Venkatesh and Suresh, S. P.},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.FSTTCS.2014.121},
  URN =		{urn:nbn:de:0030-drops-48370},
  doi =		{10.4230/LIPIcs.FSTTCS.2014.121},
  annote =	{Keywords: Synchronizing words, weighted automata, timed automata}
}
  • Refine by Author
  • 19 Markey, Nicolas
  • 10 Bouyer, Patricia
  • 4 Sankur, Ocan
  • 3 Bertrand, Nathalie
  • 2 Gardy, Patrick
  • Show More...

  • Refine by Classification
  • 4 Theory of computation → Verification by model checking
  • 3 Theory of computation → Solution concepts in game theory
  • 2 Theory of computation → Algorithmic game theory
  • 2 Theory of computation → Distributed algorithms
  • 1 Theory of computation
  • Show More...

  • Refine by Keyword
  • 5 Nash equilibria
  • 3 Verification
  • 2 Complexity
  • 2 Distributed algorithms
  • 2 Parameterized models
  • Show More...

  • Refine by Type
  • 21 document

  • Refine by Publication Year
  • 4 2015
  • 3 2022
  • 2 2010
  • 2 2011
  • 2 2014
  • Show More...

Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail
© 2023-2024 Schloss Dagstuhl – LZI GmbH Imprint Privacy Contact