Search Results

Documents authored by Hahn, Christopher

Document
DOI: 10.4230/LIPIcs.SAND.2024.14
Forming Large Patterns with Local Robots in the OBLOT Model

Authors: Christopher Hahn, Jonas Harbig, and Peter Kling

Published in: LIPIcs, Volume 292, 3rd Symposium on Algorithmic Foundations of Dynamic Networks (SAND 2024)

Abstract
In the arbitrary pattern formation problem, n autonomous, mobile robots must form an arbitrary pattern P ⊆ R². The (deterministic) robots are typically assumed to be indistinguishable, disoriented, and unable to communicate. An important distinction is whether robots have memory and/or a limited viewing range. Previous work managed to form P under a natural symmetry condition if robots have no memory but an unlimited viewing range [Masafumi Yamashita and Ichiro Suzuki, 2010] or if robots have a limited viewing range but memory [Yukiko Yamauchi and Masafumi Yamashita, 2013]. In the latter case, P is only formed in a shrunk version that has constant diameter. Without memory and with limited viewing range, forming arbitrary patterns remains an open problem. We provide a partial solution by showing that P can be formed under the same symmetry condition if the robots' initial diameter is ≤ 1. Our protocol partitions P into rotation-symmetric components and exploits the initial mutual visibility to form one cluster per component. Using a careful placement of the clusters and their robots, we show that a cluster can move in a coordinated way through its component while "drawing" P by dropping one robot per pattern coordinate.
Cite as

Christopher Hahn, Jonas Harbig, and Peter Kling. Forming Large Patterns with Local Robots in the OBLOT Model. In 3rd Symposium on Algorithmic Foundations of Dynamic Networks (SAND 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 292, pp. 14:1-14:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)

Copy BibTex To Clipboard

@InProceedings{hahn_et_al:LIPIcs.SAND.2024.14,
  author =	{Hahn, Christopher and Harbig, Jonas and Kling, Peter},
  title =	{{Forming Large Patterns with Local Robots in the OBLOT Model}},
  booktitle =	{3rd Symposium on Algorithmic Foundations of Dynamic Networks (SAND 2024)},
  pages =	{14:1--14:20},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-315-7},
  ISSN =	{1868-8969},
  year =	{2024},
  volume =	{292},
  editor =	{Casteigts, Arnaud and Kuhn, Fabian},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.SAND.2024.14},
  URN =		{urn:nbn:de:0030-drops-198924},
  doi =		{10.4230/LIPIcs.SAND.2024.14},
  annote =	{Keywords: Swarm Algorithm, Swarm Robots, Distributed Algorithm, Pattern Formation, Limited Visibility, Oblivious}
}
Document
DOI: 10.4230/LIPIcs.SAND.2022.7
Loosely-Stabilizing Phase Clocks and The Adaptive Majority Problem

Authors: Petra Berenbrink, Felix Biermeier, Christopher Hahn, and Dominik Kaaser

Published in: LIPIcs, Volume 221, 1st Symposium on Algorithmic Foundations of Dynamic Networks (SAND 2022)

Abstract
We present a loosely-stabilizing phase clock for population protocols. In the population model we are given a system of n identical agents which interact in a sequence of randomly chosen pairs. Our phase clock is leaderless and it requires O(log n) states. It runs forever and is, at any point of time, in a synchronous state w.h.p. When started in an arbitrary configuration, it recovers rapidly and enters a synchronous configuration within O(n log n) interactions w.h.p. Once the clock is synchronized, it stays in a synchronous configuration for at least poly(n) parallel time w.h.p. We use our clock to design a loosely-stabilizing protocol that solves the adaptive variant of the majority problem. We assume that the agents have either opinion A or B or they are undecided and agents can change their opinion at a rate of 1/n. The goal is to keep track which of the two opinions is (momentarily) the majority. We show that if the majority has a support of at least Ω(log n) agents and a sufficiently large bias is present, then the protocol converges to a correct output within O(n log n) interactions and stays in a correct configuration for poly(n) interactions, w.h.p.
Cite as

Petra Berenbrink, Felix Biermeier, Christopher Hahn, and Dominik Kaaser. Loosely-Stabilizing Phase Clocks and The Adaptive Majority Problem. In 1st Symposium on Algorithmic Foundations of Dynamic Networks (SAND 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 221, pp. 7:1-7:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)

Copy BibTex To Clipboard

@InProceedings{berenbrink_et_al:LIPIcs.SAND.2022.7,
  author =	{Berenbrink, Petra and Biermeier, Felix and Hahn, Christopher and Kaaser, Dominik},
  title =	{{Loosely-Stabilizing Phase Clocks and The Adaptive Majority Problem}},
  booktitle =	{1st Symposium on Algorithmic Foundations of Dynamic Networks (SAND 2022)},
  pages =	{7:1--7:17},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-224-2},
  ISSN =	{1868-8969},
  year =	{2022},
  volume =	{221},
  editor =	{Aspnes, James and Michail, Othon},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.SAND.2022.7},
  URN =		{urn:nbn:de:0030-drops-159493},
  doi =		{10.4230/LIPIcs.SAND.2022.7},
  annote =	{Keywords: Population Protocols, Phase Clocks, Loose Self-stabilization, Clock Synchronization, Majority, Adaptive}
}
Document
DOI: 10.4230/LIPIcs.CONCUR.2016.13
Deciding Hyperproperties

Authors: Bernd Finkbeiner and Christopher Hahn

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

Abstract
Hyperproperties, like observational determinism or symmetry, cannot be expressed as properties of individual computation traces, because they describe a relation between multiple computation traces. HyperLTL is a temporal logic that captures such relations through trace variables, which are introduced through existential and universal trace quantifiers and can be used to refer to multiple computations at the same time. In this paper, we study the satisfiability problem of HyperLTL. We show that the problem is PSPACE-complete for alternation-free formulas (and, hence, no more expensive than LTL satisfiability), EXPSPACE-complete for exists-forall-formulas, and undecidable for forall-exists-formulas. Many practical hyperproperties can be expressed as alternation-free formulas. Our results show that both satisfiability and implication are decidable for such properties.
Cite as

Bernd Finkbeiner and Christopher Hahn. Deciding Hyperproperties. In 27th International Conference on Concurrency Theory (CONCUR 2016). Leibniz International Proceedings in Informatics (LIPIcs), Volume 59, pp. 13:1-13:14, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2016)

Copy BibTex To Clipboard

@InProceedings{finkbeiner_et_al:LIPIcs.CONCUR.2016.13,
  author =	{Finkbeiner, Bernd and Hahn, Christopher},
  title =	{{Deciding Hyperproperties}},
  booktitle =	{27th International Conference on Concurrency Theory (CONCUR 2016)},
  pages =	{13:1--13:14},
  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.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2016.13},
  URN =		{urn:nbn:de:0030-drops-61706},
  doi =		{10.4230/LIPIcs.CONCUR.2016.13},
  annote =	{Keywords: temporal logics, satisfiability, hyperproperties, complexity}
}
© 2023-2024 Schloss Dagstuhl – LZI GmbH Imprint Privacy Contact