Arrow Research search

Author name cluster

Nancy Lynch

Possible papers associated with this exact author name in Arrow. This page groups case-insensitive exact name matches and is not a full identity disambiguation profile.

17 papers
1 author row

Possible papers

17

AAMAS Conference 2026 Conference Paper

Nanobot Algorithms for Treatment of Diffuse Cancer

  • Noble Harasha
  • Nancy Lynch

Weconsidertheproblemofaswarmofnanobots detectingandtreating human cancer that is diffuse, dispersed in a region with multiple separate cancer sites in need of treatment. We present a mathematical model of nanobots and their colloidal environment that is inspired by actual chemotactic nanoparticles, involving agents noisily following chemical gradients (both attractively and repellently, depending on the chemical). We present three incrementally sophisticated algorithms that describe additional chemical payloads that agents carry onboard, beyond the cancer-treating drug K, as well as the rules for when agents drop their payloads: Algorithm KM, in which agents simply ascend naturally existing chemical M signals that surround cancer sites; KMA, in which agents themselves amplify these natural signals by dropping chemical A payloads upon reaching a site; and KMAR, in which agents choose to either amplify the signal by dropping chemical A or counteract/reduce the signal by dropping chemical R, according to the current unsatisfied demand of the site. We present simulation results for all of the algorithms, across a set of distinct cancer arrangements, that track both the achieved treatment success as well as the time/duration of the treatment. KMhasgenerallysuccessfultreatmentunlessthenatural M-signals are weak, in which case the treatment progresses too slowly. KMA demonstrates a significant speedup in treatment time (over KM), but also a drop in success except for the most concentrated cancer patterns. KMAR has relatively optimal performance across all types of cancer patterns, demonstrating robustness and adaptability in its mechanisms for nanobot coordination.

AAMAS Conference 2023 Conference Paper

A Comparison of New Swarm Task Allocation Algorithms in Unknown Environments with Varying Task Density

  • Grace Cai
  • Noble Harasha
  • Nancy Lynch

Task allocation is an important problem for robot swarms to solve, allowing agents to reduce task completion time by performing tasks in a distributed fashion. Existing task allocation algorithms often assume prior knowledge of task location and demand or fail to consider the effects of the geometric distribution of tasks on the completion time and communication cost of the algorithms. In this paper, we examine an environment where agents must explore and discover tasks with positive demand and successfully assign themselves to complete all such tasks. We first provide a new discrete general model for modeling swarms. Operating within this theoretical framework, we propose two new task allocation algorithms for initially unknown environments – one based on N-site selection and the other on virtual pheromones. We analyze each algorithm separately and also evaluate the effectiveness of the two algorithms in dense vs. sparse task distributions. Compared to the Levy walk, which has been theorized to be optimal for foraging, our virtual pheromone inspired algorithm is much faster in sparse to medium task densities but is communication and agent intensive. Our site selection inspired algorithm also outperforms Levy walk in sparse task densities and is a less resource-intensive option than our virtual pheromone algorithm for this case. Because the performance of both algorithms relative to random walk is dependent on task density, our results shed light on how task density is important in choosing a task allocation algorithm in initially unknown environments.

TCS Journal 2020 Journal Article

Leader election in SINR model with arbitrary power control

  • Magnús M. Halldórsson
  • Stephan Holzer
  • Evangelia Anna Markatou
  • Nancy Lynch

We consider the Leader Election Problem in the Signal-to-Interference-plus-Noise-Ratio (SINR) model where nodes can adjust their transmission power. We show that in this setting it is possible to elect a leader in two communication rounds, with high probability. Previously, it was known that Θ ( log ⁡ n ) rounds were sufficient and necessary when using uniform power, where n is the number of nodes in the network. We then examine how much power control is needed to achieve fast leader election. We show that every 2-round leader election algorithm in the SINR model running correctly w. h. p. requires a power range 2 Ω ( n ), even when n is known. We complement this with an algorithm that uses power range 2 O ˜ ( n ) 1, when n is known, and 2 O ˜ ( n 1. 5 ), when n is not known. We also explore tradeoffs between time and power used, and show that to elect a leader in t rounds, a range of possible power levels of size e x p ( n 1 / Θ ( t ) ) is sufficient and necessary.

TCS Journal 2020 Journal Article

On simple back-off in unreliable radio networks

  • Seth Gilbert
  • Nancy Lynch
  • Calvin Newport
  • Dominik Pajak

In this paper, we study local and global broadcast in the dual graph model, which describes communication in a radio network with both reliable and unreliable links. Existing work proved that efficient solutions to these problems are impossible in the dual graph model under standard assumptions. In real networks, however, simple back-off strategies tend to perform well for solving these basic communication tasks. We address this apparent paradox by introducing a new set of constraints to the dual graph model that better generalize the slow/fast fading behavior common in real networks. We prove that in the context of these new constraints, simple back-off strategies now provide efficient solutions to local and global broadcast in the dual graph model. We also precisely characterize how this efficiency degrades as the new constraints are reduced down to non-existent, and prove new lower bounds that establish this degradation as near optimal for a large class of natural algorithms. We conclude with an analysis of a more general model where we propose an enhanced back-off algorithm. These results provide theoretical foundations for the practical observation that simple back-off algorithms tend to work well even amid the complicated link dynamics of real radio networks.

I&C Journal 2011 Journal Article

The impossibility of boosting distributed service resilience

  • Paul Attie
  • Rachid Guerraoui
  • Petr Kuznetsov
  • Nancy Lynch
  • Sergio Rajsbaum

We study f-resilient services, which are guaranteed to operate as long as no more than f of the associated processes fail. We prove three theorems asserting the impossibility of boosting the resilience of such services. Our first theorem allows any connection pattern between processes and services but assumes these services to be atomic (linearizable) objects. This theorem says that no distributed system in which processes coordinate using f-resilient atomic objects and reliable registers can solve the consensus problem in the presence of f + 1 undetectable process stopping failures. In contrast, we show that it is possible to boost the resilience of some systems solving problems easier than consensus: for example, the 2-set-consensus problem is solvable for 2 n processes and 2 n - 1 failures (i. e. , wait-free) using n-process consensus services resilient to n - 1 failures (wait-free). Our proof is short and self-contained. We then introduce the larger class of failure-oblivious services. These are services that cannot use information about failures, although they may behave more flexibly than atomic objects. An example of such a service is totally ordered broadcast. Our second theorem generalizes the first theorem and its proof to failure-oblivious services. Our third theorem allows the system to contain failure-aware services, such as failure detectors, in addition to failure-oblivious services. This theorem requires that each failure-aware service be connected to all processes; thus, f + 1 process failures overall can disable all the failure-aware services. In contrast, it is possible to boost the resilience of a system solving consensus using failure-aware services if arbitrary connection patterns between processes and services are allowed: consensus is solvable for any number of failures using only 1-resilient 2-process perfect failure detectors. As far as we know, this is the first time a unified framework has been used to describe both atomic and non-atomic objects, and the first time boosting analysis has been performed for services more general than atomic objects.

TAAS Journal 2009 Journal Article

Self-stabilizing robot formations over unreliable networks

  • Seth Gilbert
  • Nancy Lynch
  • Sayan Mitra
  • Tina Nolte

We describe how a set of mobile robots can arrange themselves on any specified curve on the plane in the presence of dynamic changes both in the underlying ad hoc network and in the set of participating robots. Our strategy is for the mobile robots to implement a self-stabilizing virtual layer consisting of mobile client nodes, stationary Virtual Nodes (VNs), and local broadcast communication. The VNs are associated with predetermined regions in the plane and coordinate among themselves to distribute the client nodes relatively uniformly among the VNs' regions. Each VN directs its local client nodes to align themselves on the local portion of the target curve. The resulting motion coordination protocol is self-stabilizing, in that each robot can begin the execution in any arbitrary state and at any arbitrary location in the plane. In addition, self-stabilization ensures that the robots can adapt to changes in the desired target formation.

TCS Journal 2006 Journal Article

Switched PIOA: Parallel composition via distributed scheduling

  • Ling Cheung
  • Nancy Lynch
  • Roberto Segala
  • Frits Vaandrager

This paper presents the framework of switched probabilistic input/output automata (or switched PIOA), augmenting the original PIOA framework with an explicit control exchange mechanism. Using this mechanism, we model a network of processes passing a single token among them, so that the location of this token determines which process is scheduled to make the next move. This token structure therefore implements a distributed scheduling scheme: scheduling decisions are always made by the (unique) active component. Distributed scheduling allows us to draw a clear line between local and global nondeterministic choices. We then require that local nondeterministic choices are resolved using strictly local information. This eliminates unrealistic schedules that arise under the more common centralized scheduling scheme. As a result, we are able to prove that our trace-style semantics is compositional.

I&C Journal 2003 Journal Article

Hybrid I/O automata

  • Nancy Lynch
  • Roberto Segala
  • Frits Vaandrager

Hybrid systems are systems that exhibit a combination of discrete and continuous behavior. Typical hybrid systems include computer components, which operate in discrete program steps, and real-world components, whose behavior over time intervals evolves according to physical constraints. Important examples of hybrid systems include automated transportation systems, robotics systems, process control systems, systems of embedded devices, and mobile computing systems. Such systems can be very complex, and very difficult to describe and analyze. This paper presents the Hybrid Input/Output Automaton (HIOA) modeling framework, a basic mathematical framework to support description and analysis of hybrid systems. An important feature of this model is its support for decomposing hybrid system descriptions. In particular, the framework includes a notion of external behavior for a hybrid I/O automaton, which captures its discrete and continuous interactions with its environment. The framework also defines what it means for one HIOA to implement another, based on an inclusion relationship between their external behavior sets, and defines a notion of simulation, which provides a sufficient condition for demonstrating implementation relationships. The framework also includes a composition operation for HIOAs, which respects the implementation relation and a notion of receptiveness, which implies that an HIOA does not block the passage of time. The framework is intended to support analysis methods from both computer science and control theory. This work is a simplification of our earlier HIOA model. The main simplification in the new model is a clearer separation between the mechanisms used to model discrete and continuous interaction between components. In particular, the new model removes the dual use of external variables for discrete and continuous interactions.

TCS Journal 2000 Journal Article

Revisiting the paxos algorithm

  • Roberto De Prisco
  • Butler Lampson
  • Nancy Lynch

The paxos algorithm is an efficient and highly fault-tolerant algorithm, devised by Lamport, for reaching consensus in a distributed system. Although it appears to be practical, it seems to be not widely known or understood. This paper contains a new presentation of the paxos algorithm, based on a formal decomposition into several interacting components. It also contains a correctness proof and a time performance and fault-tolerance analysis. The formal framework used for the presentation of the algorithm is provided by the Clock General Timed Automaton (Clock GTA) model. The Clock GTA provides a systematic way of describing timing-based systems in which there is a notion of “normal” timing behavior, but that do not necessarily always exhibit this “normal” timing behavior.

TCS Journal 1999 Journal Article

Eventually-serializable data services

  • Alan Fekete
  • David Gupta
  • Victor Luchangco
  • Nancy Lynch
  • Alex Shvartsman

Data replication is used in distributed systems to improve availability, increase throughput and eliminate single points of failures. The cost of replication is that significant care and communication is required to maintain consistency among replicas. In some settings, such as distributed directory services, it is acceptable to have transient inconsistencies, in exhange for better performance, as long as a consistent view of the data is eventually established. For such services to be usable, it is important that the consistency guarantees are specified clearly. We present a new specification for distributed data services that trades off immediate consistency guarantees for improved system availability and efficiency, while ensuring the long-term consistency of the data. An eventually-serializable data service maintains the requested operations in a partial order that gravitates over time towards a total order. It provides clear and unambiguous guarantees about the immediate and long-term behavior of the system. We also present an algorithm, based on the lazy replication strategy of Ladin, Liskov, Shrira, and Ghemawat (1992), that implements this specification. Our algorithm provides the external interface of the eventually-serializable data service specification, and generalizes their algorithm by allowing arbitrary operations and greater flexibility in specifying consistency requirements. In addition to correctness, we prove performance and fault-tolerance properties of this algorithm.

TCS Journal 1999 Journal Article

Timing conditions for linearizability in uniform counting networks

  • Nancy Lynch
  • Nir Shavit
  • Alex Shvartsman
  • Dan Touitou

Counting networks are concurrent data structures that serve as building blocks in the design of highly scalable concurrent data structures in a way that eliminates sequential bottlenecks and contention. Linearizable counting networks assure that the order of the values returned by the network reflects the real-time order in which they were requested. Linearizability is an important consistency condition for concurrent data structures, as it simplifies proofs and enhances compositionality. Though most counting networks are not linearizable, this paper presents a precise characterization of the timing conditions under which uniform non-linearizable networks exhibit linearizable behavior. Uniformity is a common structuring property of almost all published counting networks: a uniform network is made of “balancers” and “wires” so that each balancer lies on some path from inputs to outputs, and all paths from inputs to outputs have equal lengths. Our results include the following simple condition: if the time it takes a slow token to traverse a “wire” or “balancer” is no more than twice that of a fast token, the network is linearizable. Surprisingly, the timing measure in this condition is local to the individual “wires” and “balancers” of the network, that is, it is independent of network depth. We use our timing measure to mathematically explain our empirical findings: that in a variety of highly concurrent execution scenarios tested on a simulated shared memory multiprocessor, the Bitonic counting networks of Aspnes, Herlihy, and Shavit exhibit completely linearizable behavior, and when linearizability is violated, the percentage of violations is relatively small. Herlihy, Shavit, and Waarts have shown that counting networks that achieve linearizability under all circumstances must pay the penalty of linear time latency. Our results suggest that for systems in which timing anomalies occur infrequently, such linear delays may be an unnecessary burden on applications that are willing to incur occasional non-linearizability.

I&C Journal 1998 Journal Article

Liveness in Timed and Untimed Systems

  • Roberto Segala
  • Rainer Gawlick
  • Jørgen Søgaard-Andersen
  • Nancy Lynch

When proving the correctness of algorithms in distributed systems, one generally considerssafetyconditions andlivenessconditions. The Input/Output (I/O) automaton model and its timed version have been used successfully, but have focused on safety conditions and on a restricted form of liveness called fairness. In this paper we develop a new I/O automaton model, and a new timed I/O automaton model, that permit the verification of general liveness properties on the basis of existing verification techniques. Our models include a notion ofreceptivenesswhich extends the idea ofreceptivenessof other existing formalisms, and enables the use of compositional verification techniques. The presentation includes anembeddingof the untimed model into the timed model which preserves all the interesting attributes of the untimed model. Thus, our models constitute acoordinated frameworkfor the description of concurrent and distributed systems satisfying general liveness properties.

I&C Journal 1996 Journal Article

Forward and Backward Simulations

  • Nancy Lynch
  • Frits Vaandrager

A general automaton model for timing-based systems is presented and is used as the context for developing a variety of simulation proof techniques for such systems. These techniques include (1) refinements, (2) forward and backward simulations, (3) hybrid forward–backward and backward–forward simulations, and (4) history and prophecy relations. Relationships between the different types of simulations, as well as soundness and completeness results, are stated and proved. These results are (with one exception) analogous to the results for untimed systems in Part I of this paper. In fact, many of the results for the timed case are obtained as consequences of the analogous results for the untimed case.

TCS Journal 1995 Journal Article

Hybrid atomicity for nested transactions

  • Alan Fekete
  • Nancy Lynch
  • William E. Weihl

This paper defines the notion of hybrid atomicity for nested transaction systems, and presents and verifies an algorithm providing this property. Hybrid atomicity is a modular property; it allows the correctness of a system to be deduced from the fact that each object is implemented to have the property. It allows more concurrency than dynamic atomicity, by assigning timestamps to transactions at commit. The Avalon system provides exactly this facility. The results in this paper extend earlier work using the same model for locking and timestamp-based algorithms, providing further evidence for the generality of the approach. However, there are some subtle differences with the definitions used in earlier work, showing the difficulties of developing precise general models for nested transaction systems.

I&C Journal 1988 Journal Article

A new fault-tolerant algorithm for clock synchronization

  • Jennifer Lundelius Welch
  • Nancy Lynch

We describe a new fault-tolerant algorithm for solving a variant of Lamport's clock synchronization problem. The algorithm is designed for a system of distributed processes that communicate by sending messages. Each process has its own read-only physical clock whose drift rate from real time is very small. By adding a value to its physical clock time, the process obtaines its local time. The algorithm solves the problem of maintaining closely synchronized local times, assuming that processes' local times are closely synchronized initially. The algorithm is able to tolerate the failure of just under one-third of the participating processes. It maintains synchronization to within a small constant, whose magnitude depends upon the rate of clock drift, the message delivery time and its uncertainty, and the initial closeness of synchronization. We also give a characterization of how far the clocks drift from real time. Reintegration of a repaired process can be accomplished using a slight modification of the basic alborithm. A similar style algorithm can also be used to achieve synchronization initially.

TCS Journal 1986 Journal Article

Introduction to the theory of nested transactions

  • Nancy Lynch
  • Michael Merritt

A new formal model is presented for studying concurrency and resiliency properties for nested transactions. The model is used to state and prove correctness of a well-known locking algorithm.

TCS Journal 1978 Journal Article

Log space machines with multiple oracle tapes

  • Nancy Lynch

As an alternative to previously studied models for space-bounded relative computation, an oracle Turing machine with a space bound on its worktape and an arbitrary number of oracle tapes is considered. Basic properties of the resulting reducibilities are examined.

v2026.09.13