Search Results

Documents authored by Blondin, Michael

Document
Track B: Automata, Logic, Semantics, and Theory of Programming
DOI: 10.4230/LIPIcs.ICALP.2023.115
Population Protocols with Unordered Data

Authors: Michael Blondin and François Ladouceur

Published in: LIPIcs, Volume 261, 50th International Colloquium on Automata, Languages, and Programming (ICALP 2023)

Abstract
Population protocols form a well-established model of computation of passively mobile anonymous agents with constant-size memory. It is well known that population protocols compute Presburger-definable predicates, such as absolute majority and counting predicates. In this work, we initiate the study of population protocols operating over arbitrarily large data domains. More precisely, we introduce population protocols with unordered data as a formalism to reason about anonymous crowd computing over unordered sequences of data. We first show that it is possible to determine whether an unordered sequence from an infinite data domain has a datum with absolute majority. We then establish the expressive power of the "immediate observation" restriction of our model, namely where, in each interaction, an agent observes another agent who is unaware of the interaction.
Cite as

Michael Blondin and François Ladouceur. Population Protocols with Unordered Data. In 50th International Colloquium on Automata, Languages, and Programming (ICALP 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 261, pp. 115:1-115:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)

Copy BibTex To Clipboard

@InProceedings{blondin_et_al:LIPIcs.ICALP.2023.115,
  author =	{Blondin, Michael and Ladouceur, Fran\c{c}ois},
  title =	{{Population Protocols with Unordered Data}},
  booktitle =	{50th International Colloquium on Automata, Languages, and Programming (ICALP 2023)},
  pages =	{115:1--115:20},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-278-5},
  ISSN =	{1868-8969},
  year =	{2023},
  volume =	{261},
  editor =	{Etessami, Kousha and Feige, Uriel 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.2023.115},
  URN =		{urn:nbn:de:0030-drops-181673},
  doi =		{10.4230/LIPIcs.ICALP.2023.115},
  annote =	{Keywords: Population protocols, unordered data, colored Petri nets}
}
Document
DOI: 10.4230/LIPIcs.STACS.2020.40
Succinct Population Protocols for Presburger Arithmetic

Authors: Michael Blondin, Javier Esparza, Blaise Genest, Martin Helfrich, and Stefan Jaax

Published in: LIPIcs, Volume 154, 37th International Symposium on Theoretical Aspects of Computer Science (STACS 2020)

Abstract
In [Dana Angluin et al., 2006], Angluin et al. proved that population protocols compute exactly the predicates definable in Presburger arithmetic (PA), the first-order theory of addition. As part of this result, they presented a procedure that translates any formula φ of quantifier-free PA with remainder predicates (which has the same expressive power as full PA) into a population protocol with 2^?(poly(|φ|)) states that computes φ. More precisely, the number of states of the protocol is exponential in both the bit length of the largest coefficient in the formula, and the number of nodes of its syntax tree. In this paper, we prove that every formula φ of quantifier-free PA with remainder predicates is computable by a leaderless population protocol with ?(poly(|φ|)) states. Our proof is based on several new constructions, which may be of independent interest. Given a formula φ of quantifier-free PA with remainder predicates, a first construction produces a succinct protocol (with ?(|φ|³) leaders) that computes φ; this completes the work initiated in [Michael Blondin et al., 2018], where we constructed such protocols for a fragment of PA. For large enough inputs, we can get rid of these leaders. If the input is not large enough, then it is small, and we design another construction producing a succinct protocol with one leader that computes φ. Our last construction gets rid of this leader for small inputs.
Cite as

Michael Blondin, Javier Esparza, Blaise Genest, Martin Helfrich, and Stefan Jaax. Succinct Population Protocols for Presburger Arithmetic. In 37th International Symposium on Theoretical Aspects of Computer Science (STACS 2020). Leibniz International Proceedings in Informatics (LIPIcs), Volume 154, pp. 40:1-40:15, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020)

Copy BibTex To Clipboard

@InProceedings{blondin_et_al:LIPIcs.STACS.2020.40,
  author =	{Blondin, Michael and Esparza, Javier and Genest, Blaise and Helfrich, Martin and Jaax, Stefan},
  title =	{{Succinct Population Protocols for Presburger Arithmetic}},
  booktitle =	{37th International Symposium on Theoretical Aspects of Computer Science (STACS 2020)},
  pages =	{40:1--40:15},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-140-5},
  ISSN =	{1868-8969},
  year =	{2020},
  volume =	{154},
  editor =	{Paul, Christophe and Bl\"{a}ser, Markus},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.STACS.2020.40},
  URN =		{urn:nbn:de:0030-drops-119018},
  doi =		{10.4230/LIPIcs.STACS.2020.40},
  annote =	{Keywords: Population protocols, Presburger arithmetic, state complexity}
}
Document
DOI: 10.4230/LIPIcs.CONCUR.2019.31
Expressive Power of Broadcast Consensus Protocols

Authors: Michael Blondin, Javier Esparza, and Stefan Jaax

Published in: LIPIcs, Volume 140, 30th International Conference on Concurrency Theory (CONCUR 2019)

Abstract
Population protocols are a formal model of computation by identical, anonymous mobile agents interacting in pairs. Their computational power is rather limited: Angluin et al. have shown that they can only compute the predicates over N^k expressible in Presburger arithmetic. For this reason, several extensions of the model have been proposed, including the addition of devices called cover-time services, absence detectors, and clocks. All these extensions increase the expressive power to the class of predicates over N^k lying in the complexity class NL when the input is given in unary. However, these devices are difficult to implement, since they require that an agent atomically receives messages from all other agents in a population of unknown size; moreover, the agent must know that they have all been received. Inspired by the work of the verification community on Emerson and Namjoshi’s broadcast protocols, we show that NL-power is also achieved by extending population protocols with reliable broadcasts, a simpler, standard communication primitive.
Cite as

Michael Blondin, Javier Esparza, and Stefan Jaax. Expressive Power of Broadcast Consensus Protocols. In 30th International Conference on Concurrency Theory (CONCUR 2019). Leibniz International Proceedings in Informatics (LIPIcs), Volume 140, pp. 31:1-31:16, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019)

Copy BibTex To Clipboard

@InProceedings{blondin_et_al:LIPIcs.CONCUR.2019.31,
  author =	{Blondin, Michael and Esparza, Javier and Jaax, Stefan},
  title =	{{Expressive Power of Broadcast Consensus Protocols}},
  booktitle =	{30th International Conference on Concurrency Theory (CONCUR 2019)},
  pages =	{31:1--31:16},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-121-4},
  ISSN =	{1868-8969},
  year =	{2019},
  volume =	{140},
  editor =	{Fokkink, Wan and van Glabbeek, Rob},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2019.31},
  URN =		{urn:nbn:de:0030-drops-109330},
  doi =		{10.4230/LIPIcs.CONCUR.2019.31},
  annote =	{Keywords: population protocols, complexity theory, counter machines, distributed computing}
}
Document
DOI: 10.4230/LIPIcs.CONCUR.2018.14
Affine Extensions of Integer Vector Addition Systems with States

Authors: Michael Blondin, Christoph Haase, and Filip Mazowiecki

Published in: LIPIcs, Volume 118, 29th International Conference on Concurrency Theory (CONCUR 2018)

Abstract
We study the reachability problem for affine Z-VASS, which are integer vector addition systems with states in which transitions perform affine transformations on the counters. This problem is easily seen to be undecidable in general, and we therefore restrict ourselves to affine Z-VASS with the finite-monoid property (afmp-Z-VASS). The latter have the property that the monoid generated by the matrices appearing in their affine transformations is finite. The class of afmp-Z-VASS encompasses classical operations of counter machines such as resets, permutations, transfers and copies. We show that reachability in an afmp-Z-VASS reduces to reachability in a Z-VASS whose control-states grow polynomially in the size of the matrix monoid. Our construction shows that reachability relations of afmp-Z-VASS are semilinear, and in particular enables us to show that reachability in Z-VASS with transfers and Z-VASS with copies is PSPACE-complete.
Cite as

Michael Blondin, Christoph Haase, and Filip Mazowiecki. Affine Extensions of Integer Vector Addition Systems with States. In 29th International Conference on Concurrency Theory (CONCUR 2018). Leibniz International Proceedings in Informatics (LIPIcs), Volume 118, pp. 14:1-14:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2018)

Copy BibTex To Clipboard

@InProceedings{blondin_et_al:LIPIcs.CONCUR.2018.14,
  author =	{Blondin, Michael and Haase, Christoph and Mazowiecki, Filip},
  title =	{{Affine Extensions of Integer Vector Addition Systems with States}},
  booktitle =	{29th International Conference on Concurrency Theory (CONCUR 2018)},
  pages =	{14:1--14:17},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-087-3},
  ISSN =	{1868-8969},
  year =	{2018},
  volume =	{118},
  editor =	{Schewe, Sven and Zhang, Lijun},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2018.14},
  URN =		{urn:nbn:de:0030-drops-95520},
  doi =		{10.4230/LIPIcs.CONCUR.2018.14},
  annote =	{Keywords: Vector addition systems, affine transformations, reachability, semilinear sets, computational complexity}
}
Document
DOI: 10.4230/LIPIcs.CONCUR.2018.33
Automatic Analysis of Expected Termination Time for Population Protocols

Authors: Michael Blondin, Javier Esparza, and Antonín Kucera

Published in: LIPIcs, Volume 118, 29th International Conference on Concurrency Theory (CONCUR 2018)

Abstract
Population protocols are a formal model of sensor networks consisting of identical mobile devices. Two devices can interact and thereby change their states. Computations are infinite sequences of interactions in which the interacting devices are chosen uniformly at random. In well designed population protocols, for every initial configuration of devices, and for every computation starting at this configuration, all devices eventually agree on a consensus value. We address the problem of automatically computing a parametric bound on the expected time the protocol needs to reach this consensus. We present the first algorithm that, when successful, outputs a function f(n) such that the expected time to consensus is bound by O(f(n)), where n is the number of devices executing the protocol. We experimentally show that our algorithm terminates and provides good bounds for many of the protocols found in the literature.
Cite as

Michael Blondin, Javier Esparza, and Antonín Kucera. Automatic Analysis of Expected Termination Time for Population Protocols. In 29th International Conference on Concurrency Theory (CONCUR 2018). Leibniz International Proceedings in Informatics (LIPIcs), Volume 118, pp. 33:1-33:16, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2018)

Copy BibTex To Clipboard

@InProceedings{blondin_et_al:LIPIcs.CONCUR.2018.33,
  author =	{Blondin, Michael and Esparza, Javier and Kucera, Anton{\'\i}n},
  title =	{{Automatic Analysis of Expected Termination Time for Population Protocols}},
  booktitle =	{29th International Conference on Concurrency Theory (CONCUR 2018)},
  pages =	{33:1--33:16},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-087-3},
  ISSN =	{1868-8969},
  year =	{2018},
  volume =	{118},
  editor =	{Schewe, Sven and Zhang, Lijun},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2018.33},
  URN =		{urn:nbn:de:0030-drops-95711},
  doi =		{10.4230/LIPIcs.CONCUR.2018.33},
  annote =	{Keywords: population protocols, performance analysis, expected termination time}
}
Document
DOI: 10.4230/LIPIcs.STACS.2018.16
Large Flocks of Small Birds: on the Minimal Size of Population Protocols

Authors: Michael Blondin, Javier Esparza, and Stefan Jaax

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

Abstract
Population protocols are a well established model of distributed computation by mobile finite-state agents with very limited storage. A classical result establishes that population protocols compute exactly predicates definable in Presburger arithmetic. We initiate the study of the minimal amount of memory required to compute a given predicate as a function of its size. We present results on the predicates x >= n for n \in N, and more generally on the predicates corresponding to systems of linear inequalities. We show that they can be computed by protocols with O(log n) states (or, more generally, logarithmic in the coefficients of the predicate), and that, surprisingly, some families of predicates can be computed by protocols with O(log log n) states. We give essentially matching lower bounds for the class of 1-aware protocols.
Cite as

Michael Blondin, Javier Esparza, and Stefan Jaax. Large Flocks of Small Birds: on the Minimal Size of Population Protocols. In 35th Symposium on Theoretical Aspects of Computer Science (STACS 2018). Leibniz International Proceedings in Informatics (LIPIcs), Volume 96, pp. 16:1-16:14, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2018)

Copy BibTex To Clipboard

@InProceedings{blondin_et_al:LIPIcs.STACS.2018.16,
  author =	{Blondin, Michael and Esparza, Javier and Jaax, Stefan},
  title =	{{Large Flocks of Small Birds: on the Minimal Size of Population Protocols}},
  booktitle =	{35th Symposium on Theoretical Aspects of Computer Science (STACS 2018)},
  pages =	{16:1--16:14},
  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.dagstuhl.de/entities/document/10.4230/LIPIcs.STACS.2018.16},
  URN =		{urn:nbn:de:0030-drops-85116},
  doi =		{10.4230/LIPIcs.STACS.2018.16},
  annote =	{Keywords: Population protocols, Presburger arithmetic}
}
Document
DOI: 10.4230/LIPIcs.FSTTCS.2017.16
Forward Analysis for WSTS, Part III: Karp-Miller Trees

Authors: Michael Blondin, Alain Finkel, and Jean Goubault-Larrecq

Published in: LIPIcs, Volume 93, 37th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2017)

Abstract
This paper is a sequel of "Forward Analysis for WSTS, Part I: Completions" [STACS 2009, LZI Intl. Proc. in Informatics 3, 433–444] and "Forward Analysis for WSTS, Part II: Complete WSTS" [Logical Methods in Computer Science 8(3), 2012]. In these two papers, we provided a framework to conduct forward reachability analyses of WSTS, using finite representations of downwards-closed sets. We further develop this framework to obtain a generic Karp-Miller algorithm for the new class of very-WSTS. This allows us to show that coverability sets of very-WSTS can be computed as their finite ideal decompositions. Under natural assumptions on positive sequences, we also show that LTL model checking for very-WSTS is decidable. The termination of our procedure rests on a new notion of acceleration levels, which we study. We characterize those domains that allow for only finitely many accelerations, based on ordinal ranks.
Cite as

Michael Blondin, Alain Finkel, and Jean Goubault-Larrecq. Forward Analysis for WSTS, Part III: Karp-Miller Trees. In 37th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2017). Leibniz International Proceedings in Informatics (LIPIcs), Volume 93, pp. 16:1-16:15, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2018)

Copy BibTex To Clipboard

@InProceedings{blondin_et_al:LIPIcs.FSTTCS.2017.16,
  author =	{Blondin, Michael and Finkel, Alain and Goubault-Larrecq, Jean},
  title =	{{Forward Analysis for WSTS, Part III: Karp-Miller Trees}},
  booktitle =	{37th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2017)},
  pages =	{16:1--16:15},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-055-2},
  ISSN =	{1868-8969},
  year =	{2018},
  volume =	{93},
  editor =	{Lokam, Satya and Ramanujam, R.},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSTTCS.2017.16},
  URN =		{urn:nbn:de:0030-drops-84033},
  doi =		{10.4230/LIPIcs.FSTTCS.2017.16},
  annote =	{Keywords: WSTS, model checking, coverability, Karp-Miller algorithm, ideals}
}
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