12 Search Results for "Blondin, Michael"


Document
Track B: Automata, Logic, Semantics, and Theory of Programming
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
Invited Talk
State Complexity of Population Protocols (Invited Talk)

Authors: Javier Esparza

Published in: LIPIcs, Volume 213, 41st IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2021)


Abstract
Population protocols were introduced by Angluin et al. in 2004 to study the theoretical properties of networks of mobile sensors with very limited computational resources. They have also been proposed as a natural computing model, with molecules, cells, or microorganisms playing the role of sensors. In a population protocol an arbitrary number of indistinguishable, finite-state agents interact randomly in pairs to collectively decide if their initial global configuration satisfies a given property. The property is formalized as a predicate that maps each initial configuration to an output, 0 or 1. Starting from an initial configuration, the agents eventually agree to the correct output almost surely, and continue producing it forever. The protocol is said to stabilize to the correct output. It is well known that population protocols can decide exactly the semilinear predicates, or, equivalently, the predicates expressible in Presburger arithmetic. Current research concentrates on investigating the amount of resources needed to decide a given predicate. The standard resources, time and memory, translate for population protocols into expected time to stabilization, usually called parallel runtime, and number of states of each agent. In this talk we concentrate on the latter. A variant of population protocols allows for a leader, a distinguished finite-state agent that is added to the initial configuration and, intuitively, helps the other agents to organize the computation. In the last years my collaborators and I have obtained upper and lower bounds for the state complexity of population protocols with and without a leader. Define the state complexity of a predicate as the minimal number of states of a protocol that decides the predicate, and STATE(η) as the maximum state complexity of the predicates of size at most η, where predicates are encoded as quantifier-free formulas of Presburger arithmetic with coefficients written in binary. Using techniques from the theory of Petri nets and Vector Addition Systems, we have shown that STATE(η) is polynomially bounded, even for leaderless protocols; this improves on the exponential bound given in 2004 by Angluin and collaborators. We have also proved that STATE(η) ∈ Ω(log log η) for leaderless protocols, even for those deciding very simple predicates of the form x ≥ c for some constant c. In the talk I report on these results, and on two very recent, still unpublished results. Modulo the pending peer-review confirmation, the first result shows the existence of leaderless protocols with a polynomial number of states and linear parallel runtime, and the second, due to Leroux, gives a Ω((log log η)^{1/3}) lower bound for protocols with a leader.

Cite as

Javier Esparza. State Complexity of Population Protocols (Invited Talk). In 41st IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 213, p. 2:1, Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2021)


Copy BibTex To Clipboard

@InProceedings{esparza:LIPIcs.FSTTCS.2021.2,
  author =	{Esparza, Javier},
  title =	{{State Complexity of Population Protocols}},
  booktitle =	{41st IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2021)},
  pages =	{2:1--2:1},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-215-0},
  ISSN =	{1868-8969},
  year =	{2021},
  volume =	{213},
  editor =	{Boja\'{n}czyk, Miko{\l}aj and Chekuri, Chandra},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSTTCS.2021.2},
  URN =		{urn:nbn:de:0030-drops-155139},
  doi =		{10.4230/LIPIcs.FSTTCS.2021.2},
  annote =	{Keywords: Population protocols, state complexity, Petri nets}
}
Document
Track B: Automata, Logic, Semantics, and Theory of Programming
Rational Subsets of Baumslag-Solitar Groups

Authors: Michaël Cadilhac, Dmitry Chistikov, and Georg Zetzsche

Published in: LIPIcs, Volume 168, 47th International Colloquium on Automata, Languages, and Programming (ICALP 2020)


Abstract
We consider the rational subset membership problem for Baumslag-Solitar groups. These groups form a prominent class in the area of algorithmic group theory, and they were recently identified as an obstacle for understanding the rational subsets of GL(2,ℚ). We show that rational subset membership for Baumslag-Solitar groups BS(1,q) with q ≥ 2 is decidable and PSPACE-complete. To this end, we introduce a word representation of the elements of BS(1,q): their pointed expansion (PE), an annotated q-ary expansion. Seeing subsets of BS(1,q) as word languages, this leads to a natural notion of PE-regular subsets of BS(1,q): these are the subsets of BS(1,q) whose sets of PE are regular languages. Our proof shows that every rational subset of BS(1,q) is PE-regular. Since the class of PE-regular subsets of BS(1,q) is well-equipped with closure properties, we obtain further applications of these results. Our results imply that (i) emptiness of Boolean combinations of rational subsets is decidable, (ii) membership to each fixed rational subset of BS(1,q) is decidable in logarithmic space, and (iii) it is decidable whether a given rational subset is recognizable. In particular, it is decidable whether a given finitely generated subgroup of BS(1,q) has finite index.

Cite as

Michaël Cadilhac, Dmitry Chistikov, and Georg Zetzsche. Rational Subsets of Baumslag-Solitar Groups. In 47th International Colloquium on Automata, Languages, and Programming (ICALP 2020). Leibniz International Proceedings in Informatics (LIPIcs), Volume 168, pp. 116:1-116:16, Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2020)


Copy BibTex To Clipboard

@InProceedings{cadilhac_et_al:LIPIcs.ICALP.2020.116,
  author =	{Cadilhac, Micha\"{e}l and Chistikov, Dmitry and Zetzsche, Georg},
  title =	{{Rational Subsets of Baumslag-Solitar Groups}},
  booktitle =	{47th International Colloquium on Automata, Languages, and Programming (ICALP 2020)},
  pages =	{116:1--116:16},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-138-2},
  ISSN =	{1868-8969},
  year =	{2020},
  volume =	{168},
  editor =	{Czumaj, Artur and Dawar, Anuj and Merelli, Emanuela},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ICALP.2020.116},
  URN =		{urn:nbn:de:0030-drops-125238},
  doi =		{10.4230/LIPIcs.ICALP.2020.116},
  annote =	{Keywords: Rational subsets, Baumslag-Solitar groups, decidability, regular languages, pointed expansion}
}
Document
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
New Pumping Technique for 2-Dimensional VASS

Authors: Wojciech Czerwiński, Sławomir Lasota, Christof Löding, and Radosław Piórkowski

Published in: LIPIcs, Volume 138, 44th International Symposium on Mathematical Foundations of Computer Science (MFCS 2019)


Abstract
We propose a new pumping technique for 2-dimensional vector addition systems with states (2-VASS) building on natural geometric properties of runs. We illustrate its applicability by reproving an exponential bound on the length of the shortest accepting run, and by proving a new pumping lemma for languages of 2-VASS. The technique is expected to be useful for settling questions concerning languages of 2-VASS, e.g., for establishing decidability status of the regular separability problem.

Cite as

Wojciech Czerwiński, Sławomir Lasota, Christof Löding, and Radosław Piórkowski. New Pumping Technique for 2-Dimensional VASS. In 44th International Symposium on Mathematical Foundations of Computer Science (MFCS 2019). Leibniz International Proceedings in Informatics (LIPIcs), Volume 138, pp. 62:1-62:14, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019)


Copy BibTex To Clipboard

@InProceedings{czerwinski_et_al:LIPIcs.MFCS.2019.62,
  author =	{Czerwi\'{n}ski, Wojciech and Lasota, S{\l}awomir and L\"{o}ding, Christof and Pi\'{o}rkowski, Rados{\l}aw},
  title =	{{New Pumping Technique for 2-Dimensional VASS}},
  booktitle =	{44th International Symposium on Mathematical Foundations of Computer Science (MFCS 2019)},
  pages =	{62:1--62:14},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-117-7},
  ISSN =	{1868-8969},
  year =	{2019},
  volume =	{138},
  editor =	{Rossmanith, Peter and Heggernes, Pinar and Katoen, Joost-Pieter},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.MFCS.2019.62},
  URN =		{urn:nbn:de:0030-drops-110066},
  doi =		{10.4230/LIPIcs.MFCS.2019.62},
  annote =	{Keywords: vector addition systems with states, pumping, decidability}
}
Document
Reachability for Bounded Branching VASS

Authors: Filip Mazowiecki and Michał Pilipczuk

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


Abstract
In this paper we consider the reachability problem for bounded branching VASS. Bounded VASS are a variant of the classic VASS model where all values in all configurations are upper bounded by a fixed natural number, encoded in binary in the input. This model gained a lot of attention in 2012 when Haase et al. showed its connections with timed automata. Later in 2013 Fearnley and Jurdziński proved that the reachability problem in this model is PSPACE-complete even in dimension 1. Here, we investigate the complexity of the reachability problem when the model is extended with branching transitions, and we prove that the problem is EXPTIME-complete when the dimension is 2 or larger.

Cite as

Filip Mazowiecki and Michał Pilipczuk. Reachability for Bounded Branching VASS. In 30th International Conference on Concurrency Theory (CONCUR 2019). Leibniz International Proceedings in Informatics (LIPIcs), Volume 140, pp. 28:1-28:13, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019)


Copy BibTex To Clipboard

@InProceedings{mazowiecki_et_al:LIPIcs.CONCUR.2019.28,
  author =	{Mazowiecki, Filip and Pilipczuk, Micha{\l}},
  title =	{{Reachability for Bounded Branching VASS}},
  booktitle =	{30th International Conference on Concurrency Theory (CONCUR 2019)},
  pages =	{28:1--28:13},
  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.28},
  URN =		{urn:nbn:de:0030-drops-109303},
  doi =		{10.4230/LIPIcs.CONCUR.2019.28},
  annote =	{Keywords: Branching VASS, counter machines, reachability problem, bobrvass}
}
Document
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
Invited Talk
Petri Net Reachability Problem (Invited Talk)

Authors: Jérôme Leroux

Published in: LIPIcs, Volume 138, 44th International Symposium on Mathematical Foundations of Computer Science (MFCS 2019)


Abstract
Petri nets, also known as vector addition systems, are a long established model of concurrency with extensive applications in modelling and analysis of hardware, software and database systems, as well as chemical, biological and business processes. The central algorithmic problem for Petri nets is reachability: whether from the given initial configuration there exists a sequence of valid execution steps that reaches the given final configuration. The complexity of the problem has remained unsettled since the 1960s, and it is one of the most prominent open questions in the theory of verification. In this presentation, we overview decidability and complexity results over the last fifty years about the Petri net reachability problem.

Cite as

Jérôme Leroux. Petri Net Reachability Problem (Invited Talk). In 44th International Symposium on Mathematical Foundations of Computer Science (MFCS 2019). Leibniz International Proceedings in Informatics (LIPIcs), Volume 138, pp. 5:1-5:3, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019)


Copy BibTex To Clipboard

@InProceedings{leroux:LIPIcs.MFCS.2019.5,
  author =	{Leroux, J\'{e}r\^{o}me},
  title =	{{Petri Net Reachability Problem}},
  booktitle =	{44th International Symposium on Mathematical Foundations of Computer Science (MFCS 2019)},
  pages =	{5:1--5:3},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-117-7},
  ISSN =	{1868-8969},
  year =	{2019},
  volume =	{138},
  editor =	{Rossmanith, Peter and Heggernes, Pinar and Katoen, Joost-Pieter},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.MFCS.2019.5},
  URN =		{urn:nbn:de:0030-drops-109493},
  doi =		{10.4230/LIPIcs.MFCS.2019.5},
  annote =	{Keywords: Petri net, Reachability problem, Formal verification, Concurrency}
}
Document
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
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
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
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}
}
  • Refine by Author
  • 7 Blondin, Michael
  • 5 Esparza, Javier
  • 3 Jaax, Stefan
  • 2 Mazowiecki, Filip
  • 1 Cadilhac, Michaël
  • Show More...

  • Refine by Classification
  • 5 Theory of computation → Automata over infinite objects
  • 5 Theory of computation → Distributed computing models
  • 4 Theory of computation → Logic and verification
  • 3 Theory of computation → Models of computation
  • 2 Theory of computation → Complexity classes
  • Show More...

  • Refine by Keyword
  • 4 Population protocols
  • 2 Presburger arithmetic
  • 2 counter machines
  • 2 decidability
  • 2 population protocols
  • Show More...

  • Refine by Type
  • 12 document

  • Refine by Publication Year
  • 4 2018
  • 4 2019
  • 2 2020
  • 1 2021
  • 1 2023

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