4 Search Results for "Guillou, Lucie"

Document
Track B: Automata, Logic, Semantics, and Theory of Programming
DOI: 10.4230/LIPIcs.ICALP.2026.167
Population Protocols over Ordered Agents

Authors: Michael Blondin, Michaël Cadilhac, Benjamin Courchesne, Lucie Guillou, Corto Mascle, and Isa Vialard

Published in: LIPIcs, Volume 374, 53rd International Colloquium on Automata, Languages, and Programming (ICALP 2026)

Abstract
Population protocols are a distributed computation model in which a collection of anonymous, finite-state agents interact in randomly chosen pairs and update their states according to a fixed transition function. The computation is defined by the eventual stabilization of the population to a consensus that represents the output. In practice, it is natural to allow each agent to carry a unique identifier and compare it with that of another agent before interacting. We model this extension by having agents be totally ordered and interactions between two agents to be fireable only if their pair of identifiers falls in some condition set. For instance, PP[<] allows for two agents to interact only if the first one appears before the second one. We study population protocols over ordered agents PP[𝒩] where 𝒩 is a set of predicates available to restrict transition firing. We also study IO-PP[𝒩], the immediate observation fragment of PP[𝒩] where only one agent changes state per interaction. Our main result is that IO-PP[<] recognizes exactly the unambiguous star-free languages, which admits many other characterizations, such as two-variable first-order logic or two-way deterministic partially-ordered automata. We also provide a logic and an automaton model that fits in PP[<]. We further show that if the successor predicate appears in a set 𝒩 of NSPACE(n)-computable predicates, then IO-PP[𝒩] = PP[𝒩] = NSPACE(n). Finally, we investigate the problem of deciding whether a given population protocol always stabilizes to a consensus. While this problem is decidable for unordered population protocols, we show that this is undecidable already for PP[<] and IO-PP[+1], but conditionally decidable for IO-PP[<].
Cite as

Michael Blondin, Michaël Cadilhac, Benjamin Courchesne, Lucie Guillou, Corto Mascle, and Isa Vialard. Population Protocols over Ordered Agents. In 53rd International Colloquium on Automata, Languages, and Programming (ICALP 2026). Leibniz International Proceedings in Informatics (LIPIcs), Volume 374, pp. 167:1-167:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026)

Copy BibTex To Clipboard

@InProceedings{blondin_et_al:LIPIcs.ICALP.2026.167,
  author =	{Blondin, Michael and Cadilhac, Micha\"{e}l and Courchesne, Benjamin and Guillou, Lucie and Mascle, Corto and Vialard, Isa},
  title =	{{Population Protocols over Ordered Agents}},
  booktitle =	{53rd International Colloquium on Automata, Languages, and Programming (ICALP 2026)},
  pages =	{167:1--167:20},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-428-4},
  ISSN =	{1868-8969},
  year =	{2026},
  volume =	{374},
  editor =	{Bhattacharya, Sayan and Nanongkai, Danupon and Benedikt, Michael and Puppis, Gabriele},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ICALP.2026.167},
  URN =		{urn:nbn:de:0030-drops-265557},
  doi =		{10.4230/LIPIcs.ICALP.2026.167},
  annote =	{Keywords: Population protocols, First-order logic, Partially-ordered automata, Unambiguous star-free languages}
}
Document
DOI: 10.4230/LIPIcs.MFCS.2025.53
Wait-Only Broadcast Protocols Are Easier to Verify

Authors: Lucie Guillou, Arnaud Sangnier, and Nathalie Sznajder

Published in: LIPIcs, Volume 345, 50th International Symposium on Mathematical Foundations of Computer Science (MFCS 2025)

Abstract
We study networks of processes that all execute the same finite-state protocol and communicate via broadcasts. We are interested in two problems with a parameterized number of processes: the synchronization problem which asks whether there is an execution which puts all processes on a given state; and the repeated coverability problem which asks if there is an infinite execution where a given transition is taken infinitely often. Since both problems are undecidable in the general case, we investigate those problems when the protocol is Wait-Only, i.e., it has no state from which a process can both broadcast and receive messages. We establish that the synchronization problem becomes Ackermann-complete, and the repeated coverability problem is in ExpSpace and PSpace-hard.
Cite as

Lucie Guillou, Arnaud Sangnier, and Nathalie Sznajder. Wait-Only Broadcast Protocols Are Easier to Verify. In 50th International Symposium on Mathematical Foundations of Computer Science (MFCS 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 345, pp. 53:1-53:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@InProceedings{guillou_et_al:LIPIcs.MFCS.2025.53,
  author =	{Guillou, Lucie and Sangnier, Arnaud and Sznajder, Nathalie},
  title =	{{Wait-Only Broadcast Protocols Are Easier to Verify}},
  booktitle =	{50th International Symposium on Mathematical Foundations of Computer Science (MFCS 2025)},
  pages =	{53:1--53:17},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-388-1},
  ISSN =	{1868-8969},
  year =	{2025},
  volume =	{345},
  editor =	{Gawrychowski, Pawe{\l} and Mazowiecki, Filip and Skrzypczak, Micha{\l}},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.MFCS.2025.53},
  URN =		{urn:nbn:de:0030-drops-241609},
  doi =		{10.4230/LIPIcs.MFCS.2025.53},
  annote =	{Keywords: Parameterised verification, Reachability, Broadcast}
}
Document
DOI: 10.4230/LIPIcs.CONCUR.2024.26
Phase-Bounded Broadcast Networks over Topologies of Communication

Authors: Lucie Guillou, Arnaud Sangnier, and Nathalie Sznajder

Published in: LIPIcs, Volume 311, 35th International Conference on Concurrency Theory (CONCUR 2024)

Abstract
We study networks of processes that all execute the same finite state protocol and that communicate through broadcasts. The processes are organized in a graph (a topology) and only the neighbors of a process in this graph can receive its broadcasts. The coverability problem asks, given a protocol and a state of the protocol, whether there is a topology for the processes such that one of them (at least) reaches the given state. This problem is undecidable [G. Delzanno et al., 2010]. We study here an under-approximation of the problem where processes alternate a bounded number of times k between phases of broadcasting and phases of receiving messages. We show that, if the problem remains undecidable when k is greater than 6, it becomes decidable for k = 2, and ExpSpace-complete for k = 1. Furthermore, we show that if we restrict ourselves to line topologies, the problem is in P for k = 1 and k = 2.
Cite as

Lucie Guillou, Arnaud Sangnier, and Nathalie Sznajder. Phase-Bounded Broadcast Networks over Topologies of Communication. In 35th International Conference on Concurrency Theory (CONCUR 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 311, pp. 26:1-26:16, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)

Copy BibTex To Clipboard

@InProceedings{guillou_et_al:LIPIcs.CONCUR.2024.26,
  author =	{Guillou, Lucie and Sangnier, Arnaud and Sznajder, Nathalie},
  title =	{{Phase-Bounded Broadcast Networks over Topologies of Communication}},
  booktitle =	{35th International Conference on Concurrency Theory (CONCUR 2024)},
  pages =	{26:1--26:16},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-339-3},
  ISSN =	{1868-8969},
  year =	{2024},
  volume =	{311},
  editor =	{Majumdar, Rupak and Silva, Alexandra},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2024.26},
  URN =		{urn:nbn:de:0030-drops-207987},
  doi =		{10.4230/LIPIcs.CONCUR.2024.26},
  annote =	{Keywords: Parameterized verification, Coverability, Broadcast Networks}
}
Document
DOI: 10.4230/LIPIcs.CONCUR.2023.7
Safety Analysis of Parameterised Networks with Non-Blocking Rendez-Vous

Authors: Lucie Guillou, Arnaud Sangnier, and Nathalie Sznajder

Published in: LIPIcs, Volume 279, 34th International Conference on Concurrency Theory (CONCUR 2023)

Abstract
We consider networks of processes that all execute the same finite-state protocol and communicate via a rendez-vous mechanism. When a process requests a rendez-vous, another process can respond to it and they both change their control states accordingly. We focus here on a specific semantics, called non-blocking, where the process requesting a rendez-vous can change its state even if no process can respond to it. In this context, we study the parameterised coverability problem of a configuration, which consists in determining whether there is an initial number of processes and an execution allowing to reach a configuration bigger than a given one. We show that this problem is EXPSPACE-complete and can be solved in polynomial time if the protocol is partitioned into two sets of states, the states from which a process can request a rendez-vous and the ones from which it can answer one. We also prove that the problem of the existence of an execution bringing all the processes in a final state is undecidable in our context. These two problems can be solved in polynomial time with the classical rendez-vous semantics.
Cite as

Lucie Guillou, Arnaud Sangnier, and Nathalie Sznajder. Safety Analysis of Parameterised Networks with Non-Blocking Rendez-Vous. In 34th International Conference on Concurrency Theory (CONCUR 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 279, pp. 7:1-7:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)

Copy BibTex To Clipboard

@InProceedings{guillou_et_al:LIPIcs.CONCUR.2023.7,
  author =	{Guillou, Lucie and Sangnier, Arnaud and Sznajder, Nathalie},
  title =	{{Safety Analysis of Parameterised Networks with Non-Blocking Rendez-Vous}},
  booktitle =	{34th International Conference on Concurrency Theory (CONCUR 2023)},
  pages =	{7:1--7:17},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-299-0},
  ISSN =	{1868-8969},
  year =	{2023},
  volume =	{279},
  editor =	{P\'{e}rez, Guillermo A. and Raskin, Jean-Fran\c{c}ois},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2023.7},
  URN =		{urn:nbn:de:0030-drops-190015},
  doi =		{10.4230/LIPIcs.CONCUR.2023.7},
  annote =	{Keywords: Parameterised verification, Coverability, Counter machines}
}
  • Refine by Type
  • 4 Document/PDF
  • 1 Document/HTML

  • Refine by Publication Year
  • 1 2026
  • 1 2025
  • 1 2024
  • 1 2023

  • Refine by Author
  • 4 Guillou, Lucie
  • 3 Sangnier, Arnaud
  • 3 Sznajder, Nathalie
  • 1 Blondin, Michael
  • 1 Cadilhac, Michaël
  • Show More...

  • Refine by Series/Journal
  • 4 LIPIcs

  • Refine by Classification
  • 4 Theory of computation → Formal languages and automata theory
  • 1 Theory of computation → Distributed computing models
  • 1 Theory of computation → Logic and verification

  • Refine by Keyword
  • 2 Coverability
  • 2 Parameterised verification
  • 1 Broadcast
  • 1 Broadcast Networks
  • 1 Counter machines
  • Show More...

Any Issues?
X

Feedback on the Current Page

CAPTCHA

Thanks for your feedback!

Feedback submitted to Dagstuhl Publishing

Could not send message

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