https://hdl.handle.net/1721.1/143999 Sun, 12 Apr 2026 03:04:25 GMT 2026-04-12T03:04:25Z https://hdl.handle.net/1721.1/97014 A (Truly) Local Broadcast Layer for Unreliable Radio Networks Lynch, Nancy; Newport, Calvin In this paper, we implement an efficient local broadcast service for the dual graph model, which describes communication in a radio network with both reliable and unreliable links. Our local broadcast service offers probabilistic latency guarantees for: (1) message delivery to all reliable neighbors (i.e., neighbors connected by reliable links), and (2) receiving some message when one or more reliable neighbors are broadcasting. This service significantly simplifies the design and analysis of algorithms for the otherwise challenging dual graph model. To this end, we also note that our solution can be interpreted as an implementation of the abstract MAC layer specification---therefore translating the growing corpus of algorithmic results studied on top of this layer to the dual graph model. At the core of our service is a seed agreement routine which enables nodes in the network to achieve "good enough" coordination to overcome the difficulties of unpredictable link behavior. Because this routine has potential application to other problems in this setting, we capture it with a formal specification---simplifying its reuse in other algorithms. Finally, we note that in a break from much work on distributed radio network algorithms, our problem definitions (including error bounds), implementation, and analysis do not depend on global network parameters such as the network size, a goal which required new analysis techniques. We argue that breaking the dependence of these algorithms on global parameters makes more sense and aligns better with the rise of ubiquitous computing, where devices will be increasingly working locally in an otherwise massive network. Our push for locality, in other words, is a contribution independent of the specific radio network model and problem studied here. Mon, 18 May 2015 00:00:00 GMT https://hdl.handle.net/1721.1/97014 2015-05-18T00:00:00Z https://hdl.handle.net/1721.1/95775 Consensus using Asynchronous Failure Detectors Lynch, Nancy; Sastry, Srikanth The FLP result shows that crash-tolerant consensus is impossible to solve in asynchronous systems, and several solutions have been proposed for crash-tolerant consensus under alternative (stronger) models. One popular approach is to augment the asynchronous system with appropriate failure detectors, which provide (potentially unreliable) information about process crashes in the system, to circumvent the FLP impossibility. In this paper, we demonstrate the exact mechanism by which (sufficiently powerful) asynchronous failure detectors enable solving crash-tolerant consensus. Our approach, which borrows arguments from the FLP impossibility proof and the famous result from CHT, which shows that Omega is a weakest failure detector to solve consensus, also yields a natural proof to Omega as a weakest asynchronous failure detector to solve consensus. The use of I/O automata theory in our approach enables us to model execution in a more detailed fashion than CHT and also addresses the latent assumptions and assertions in the original result in CHT. Mon, 02 Mar 2015 00:00:00 GMT https://hdl.handle.net/1721.1/95775 2015-03-02T00:00:00Z https://hdl.handle.net/1721.1/88551 A Coded Shared Atomic Memory Algorithm for Message Passing Architectures Cadambe, Viveck R.; Lynch, Nancy; Medard, Muriel; Musial, Peter This paper considers the communication and storage costs of emulating atomic (linearizable) multi-writer multi-reader shared memory in distributed message-passing systems. The paper contains three main contributions: (1) We present a atomic shared-memory emulation algorithm that we call Coded Atomic Storage (CAS). This algorithm uses erasure coding methods. In a storage system with 'N' servers that is resilient to 'f' server failures, we show that the communication cost of CAS is N/(N-2f) . The storage cost of CAS is unbounded. (2) We present a modification of the CAS algorithm known as CAS with Garbage Collection (CASGC). The CASGC algorithm is parametrized by an integer 'd' and has a bounded storage cost. We show that in every execution where the number of write operations that are concurrent with a read operation is no bigger than 'd', the CASGC algorithm with parameter 'd' satisfies atomicity and liveness. We explicitly characterize the storage cost of CASGC, and show that it has the same communication cost as CASGC. (3) We describe an algorithm known as the Communication Cost Optimal Atomic Storage (CCOAS) algorithm that achieves a smaller communication cost than CAS and CASGC. In particular, CCOAS incurs read and write communication costs of N/(N-f) measured in terms of number of object values. We also discuss drawbacks of CCOAS as compared with CAS and CASGC. Fri, 01 Aug 2014 00:00:00 GMT https://hdl.handle.net/1721.1/88551 2014-08-01T00:00:00Z https://hdl.handle.net/1721.1/81371 Asynchronous Failure Detectors Cornejo, Alejandro; Lynch, Nancy; Sastry, Srikanth Failure detectors -- oracles that provide information about process crashes -- are an important abstraction for crash tolerance in distributed systems. The generality of failure-detector theory, while providing great expressiveness, poses significant challenges in developing a robust hierarchy of failure detectors. We address some of these challenges by proposing (1) a variant of failure detectors called asynchronous failure detectors and (2) an associated modeling framework. Unlike the traditional failure-detector framework, our framework eschews real-time completely. We show that asynchronous failure detectors are sufficiently expressive to include several popular failure detectors including, but not limited to, the canonical Chandra-Toueg failure detectors, Sigma and other quorum failure detectors, Omega, anti-Omega, Omega^k, and Psi_k. Additionally, asynchronous failure detectors satisfy many desirable properties: they are self-implementable, guarantee that stronger asynchronous failure-detectors solve harder problems, and ensure that their outputs encode no information other than the set of crashed processes. We introduce the notion of a failure detector being representative for a problem to capture the idea that some problems encode the same information about process crashes as their weakest failure detectors do. We show that a large class of problems, called bounded problems, do not have representative failure detectors. Finally, we use the asynchronous failure-detector framework to show how sufficiently strong AFDs circumvent the impossibility of consensus in asynchronous systems. This report supersedes MIT-CSAIL-TR-2013-002. Thu, 10 Oct 2013 00:00:00 GMT https://hdl.handle.net/1721.1/81371 2013-10-10T00:00:00Z https://hdl.handle.net/1721.1/79606 Coded Emulation of Shared Atomic Memory for Message Passing Architectures Cadambe, Viveck R.; Lynch, Nancy; Medard, Muriel; Musial, Peter This paper considers the communication and storage costs of emulating atomic (linearizable) read/write shared memory in distributed message-passing systems. We analyze the costs of previously-proposed algorithms by Attiya, Bar-Noy, and Dolev (the ABD algorithm) and by Fan and Lynch (the LDR algorithm), and develop new coding-based algorithms that significantly reduce these costs. The paper contains three main contributions: (1) We present a new shared-memory algorithm that we call CAS, for Coded Atomic Storage. This algorithm uses erasure coding methods. (2) In a storage system with N servers that is resilient to f server failures, we show that the communication costs for the ABD and LDR algorithms, measured in terms of number of object values, are both at least f + 1, whereas the communication cost for CAS is N/(N-2f). (3) We also explicitly quantify the storage costs of the ABD, LDR, and CAS algorithms. The storage cost of the ABD algorithm, measured in terms of number of object values, is N; whereas the storage costs of the LDR and CAS algorithms are both unbounded. We present a modification of the CAS algorithm based on the idea of garbage collection. The modified version of CAS has a storage cost of (d + 1) N/(N-2f), where d in an upper bound on the number of operations that are concurrent with a read operation. Thus, if d is sufficiently small, the storage cost of CAS is lower than those of both the ABD and LDR algorithms. Wed, 17 Jul 2013 00:00:00 GMT https://hdl.handle.net/1721.1/79606 2013-07-17T00:00:00Z https://hdl.handle.net/1721.1/79420 Dynamic Input/Output Automata: a Formal and Compositional Model for Dynamic Systems Attie, Paul C.; Lynch, Nancy A. We present dynamic I/O automata (DIOA), a compositional model of dynamic systems, based on I/O automata. In our model, automata can be created and destroyed dynamically, as computation proceeds. In addition, an automaton can dynamically change its signature, that is, the set of actions in which it can participate. This allows us to model mobility, by enforcing the constraint that only automata at the same location may synchronize on common actions. Our model features operators for parallel composition, action hiding, and action renaming. It also features a notion of automaton creation, and a notion of trace inclusion from one dynamic system to another, which can be used to prove that one system implements the other. Our model is hierarchical: a dynamically changing system of interacting automata is itself modeled as a single automaton that is "one level higher." This can be repeated, so that an automaton that represents such a dynamic system can itself be created and destroyed. We can thus model the addition and removal of entire subsystems with a single action. We establish fundamental compositionality results for DIOA: if one component is replaced by another whose traces are a subset of the former, then the set of traces of the system as a whole can only be reduced, and not increased, i.e., no new behaviors are added. That is, parallel composition, action hiding, and action renaming, are all monotonic with respect to trace inclusion. We also show that, under certain technical conditions, automaton creation is monotonic with respect to trace inclusion: if a system creates automaton Ai instead of (previously) creating automaton A'i, and the traces of Ai are a subset of the traces of A'i,then the set of traces of the overall system is possibly reduced, but not increased. Our trace inclusion results imply that trace equivalence is a congruence relation with respect to parallel composition, action hiding, and action renaming. Our trace inclusion results enable a design and refinement methodology based solely on the notion of externally visible behavior, and which is therefore independent of specific methods of establishing trace inclusion. It permits the refinement of components and subsystems in isolation from the entire system, and provides more flexibility in refinement than a methodology which is, for example, based on the monotonicity of forward simulation with respect to parallel composition. In the latter, every automaton must be refined using forward simulation, whereas in our framework different automata can be refined using different methods. The DIOA model was defined to support the analysis of mobile agent systems, in a joint project with researchers at Nippon Telegraph and Telephone. It can also be used for other forms of dynamic systems, such as systems described by means of object-oriented programs, and systems containing services with changing access permissions. Mon, 08 Jul 2013 00:00:00 GMT https://hdl.handle.net/1721.1/79420 2013-07-08T00:00:00Z https://hdl.handle.net/1721.1/78359 Task-Structured Probabilistic I/O Automata Canetti, Ran; Cheung, Ling; Kaynar, Dilsun; Liskov, Moses; Lynch, Nancy; Pereira, Olivier; Segala, Roberto Modeling frameworks such as Probabilistic I/O Automata (PIOA) and Markov Decision Processes permit both probabilistic and nondeterministic choices. In order to use these frameworks to express claims about probabilities of events, one needs mechanisms for resolving nondeterministic choices. For PIOAs, nondeterministic choices have traditionally been resolved by schedulers that have perfect information about the past execution. However, these schedulers are too powerful for certain settings, such as cryptographic protocol analysis, where information must sometimes be hidden. Here, we propose a new, less powerful nondeterminism-resolution mechanism for PIOAs, consisting of tasks and local schedulers. Tasks are equivalence classes of system actions that are scheduled by oblivious, global task sequences. Local schedulers resolve nondeterminism within system components, based on local information only. The resulting task-PIOA framework yields simple notions of external behavior and implementation, and supports simple compositionality results. We also define a new kind of simulation relation, and show it to be sound for proving implementation. We illustrate the potential of the task-PIOAframework by outlining its use in verifying an Oblivious Transfer protocol. "May 28, 2009." Thu, 01 Jan 2009 00:00:00 GMT https://hdl.handle.net/1721.1/78359 2009-01-01T00:00:00Z https://hdl.handle.net/1721.1/76716 Asynchronous Failure Detectors Cornejo, Alejandro; Lynch, Nancy; Sastry, Srikanth Failure detectors -- oracles that provide information about process crashes -- are an important abstraction for crash tolerance in distributed systems. The generality of failure-detector theory, while providing great expressiveness, poses significant challenges in developing a robust hierarchy of failure detectors. We address some of these challenges by proposing (1) a variant of failure detectors called asynchronous failure detectors and (2) an associated modeling framework. Unlike the traditional failure-detector framework, our framework eschews real-time completely. We show that asynchronous failure detectors are sufficiently expressive to include several popular failure detectors including, but not limited to, the canonical Chandra-Toueg failure detectors, Sigma and other quorum failure detectors, Omega, anti-Omega, Omega^k, and Psi_k. Additionally, asynchronous failure detectors satisfy many desirable properties: they are self-implementable, guarantee that stronger asynchronous failure-detectors solve harder problems, and ensure that their outputs encode no information other than the set of crashed processes. We introduce the notion of a failure detector being representative for a problem to capture the idea that some problems encode the same information about process crashes as their weakest failure detectors do. We show that a large class of problems, called bounded problems, do not have representative failure detectors. Finally, we use the asynchronous failure-detector framework to show how sufficiently strong AFDs circumvent the impossibility of consensus in asynchronous systems. This report is superseded by MIT-CSAIL-TR-2013-025. Wed, 30 Jan 2013 00:00:00 GMT https://hdl.handle.net/1721.1/76716 2013-01-30T00:00:00Z https://hdl.handle.net/1721.1/72536 Bounded-Contention Coding for Wireless Networks in the High SNR Regime Censor-Hillel, Keren; Haeupler, Bernhard; Lynch, Nancy; Medard, Muriel Efficient communication in wireless networks is typically challenged by the possibility of interference among several transmitting nodes. Much important research has been invested in decreasing the number of collisions in order to obtain faster algorithms for communication in such networks. This paper proposes a novel approach for wireless communication, which embraces collisions rather than avoiding them, over an additive channel. It introduces a coding technique called Bounded-Contention Coding (BCC) that allows collisions to be successfully decoded by the receiving nodes into the original transmissions and whose complexity depends on a bound on the contention among the transmitters. BCC enables deterministic local broadcast in a network with n nodes and at most a transmitters with information of L bits each within O(a log n + aL) bits of communication with full-duplex radios, and O((a log n + aL)(log n)) bits, with high probability, with half-duplex radios. When combined with random linear network coding, BCC gives global broadcast within O((D + a + log n)(a log n + L)) bits, with high probability. This also holds in dynamic networks that can change arbitrarily over time by a worst-case adversary. When no bound on the contention is given, it is shown how to probabilistically estimate it and obtain global broadcast that is adaptive to the true contention in the network. Mon, 27 Aug 2012 00:00:00 GMT https://hdl.handle.net/1721.1/72536 2012-08-27T00:00:00Z https://hdl.handle.net/1721.1/67885 Structuring Unreliable Radio Networks Censor-Hillel, Keren; Gilbert, Seth; Kuhn, Fabian; Lynch, Nancy; Newport, Calvin In this paper we study the problem of building a connected dominating set with constant degree (CCDS) in the dual graph radio network model. This model includes two types of links: reliable links, which always deliver messages, and unreliable links, which sometimes fail to deliver messages. Real networks compensate for this differing quality by deploying low-layer detection protocols to filter unreliable from reliable links. With this in mind, we begin by presenting an algorithm that solves the CCDS problem in the dual graph model under the assumption that every process u is provided with a local "link detector set" consisting of every neighbor connected to u by a reliable link. The algorithm solves the CCDS problem in O((Delta log2(n)/b) + log3(n)) rounds, with high probability, where Delta is the maximum degree in the reliable link graph, n is the network size, and b is an upper bound in bits on the message size. The algorithm works by first building a Maximal Independent Set (MIS) in log3(n) time, and then leveraging the local topology knowledge to efficiently connect nearby MIS processes. A natural follow up question is whether the link detector must be perfectly reliable to solve the CCDS problem. To answer this question, we first describe an algorithm that builds a CCDS in O(Delta polylog(n)) time under the assumption of O(1) unreliable links included in each link detector set. We then prove this algorithm to be (almost) tight by showing that the possible inclusion of only a single unreliable link in each process's local link detector set is sufficient to require Omega(Delta) rounds to solve the CCDS problem, regardless of message size. We conclude by discussing how to apply our algorithm in the setting where the topology of reliable and unreliable links can change over time. Thu, 22 Dec 2011 00:00:00 GMT https://hdl.handle.net/1721.1/67885 2011-12-22T00:00:00Z https://hdl.handle.net/1721.1/66224 Leader Election Using Loneliness Detection Ghaffari, Mohsen; Lynch, Nancy; Sastry, Srikanth We consider the problem of leader election (LE) in single-hop radio networks with synchronized time slots for transmitting and receiving messages. We assume that the actual number n of processes is unknown, while the size u of the ID space is known, but is possibly much larger. We consider two types of collision detection: strong (SCD), whereby all processes detect collisions, and weak (WCD), whereby only non-transmitting processes detect collisions. We introduce loneliness detection (LD) as a key subproblem for solving LE in WCD systems. LD informs all processes whether the system contains exactly one process or more than one. We show that LD captures the difference in power between SCD and WCD, by providing an implementation of SCD over WCD and LD. We present two algorithms that solve deterministic and probabilistic LD in WCD systems with time costs of O(log(u/n)) and O(min(log(u/n), (log(1/epsilon)/n)), respectively, where epsilon is the error probability. We also provide matching lower bounds. We present two algorithms that solve deterministic and probabilistic LE in SCD systems with time costs of O(log u) and O(min(log u, loglog n + log(1/epsilon))), respectively, where epsilon is the error probability. We provide matching lower bounds. Wed, 12 Oct 2011 00:00:00 GMT https://hdl.handle.net/1721.1/66224 2011-10-12T00:00:00Z https://hdl.handle.net/1721.1/62295 Partial Reversal Acyclicity Radeva, Tsvetomira; Lynch, Nancy Partial Reversal (PR) is a link reversal algorithm which ensures that the underlying graph structure is destination-oriented and acyclic. These properties of PR make it useful in routing protocols and algorithms for solving leader election and mutual exclusion. While proofs exist to establish the acyclicity property of PR, they rely on assigning labels to either the nodes or the edges in the graph. In this work we present simpler direct proof of the acyclicity property of partial reversal without using any external or dynamic labeling mechanism. First, we provide a simple variant of the PR algorithm, and show that it maintains acyclicity. Next, we present a binary relation which maps the original PR algorithm to the new algorithm, and finally, we conclude that the acyclicity proof applies to the original PR algorithm as well. Thu, 14 Apr 2011 00:00:00 GMT https://hdl.handle.net/1721.1/62295 2011-04-14T00:00:00Z https://hdl.handle.net/1721.1/61391 Decomposing Broadcast Algorithms Using Abstract MAC Layers Khabbazian, Majid; Kowalski, Dariusz; Kuhn, Fabian; Lynch, Nancy In much of the theoretical literature on global broadcast algorithms for wireless networks, issues of message dissemination are considered together with issues of contention management. This combination leads to complicated algorithms and analysis, and makes it difficult to extend the work to more difficult communication problems. In this paper, we present results aimed at simplifying such algorithms and analysis by decomposing the treatment into two levels, using abstract "MAC layer" specifications to encapsulate contention management. We use two different abstract MAC layers: the basic layer of Kuhn, Lynch, and Newport, and a new probabilistic layer. We first present a typical randomized contention-management algorithm for a standard graph-based radio network model and show that it implements both abstract MAC layers. Then we combine this algorithm with greedy algorithms for single-message and multi-message global broadcast and analyze the combinations, using both abstract MAC layers as intermediate layers. Using the basic MAC layer, we prove a bound of O(D log(n / epsilon) log(Delta)) for the time to deliver a single message everywhere with probability 1 - epsilon, where D is the network diameter, n is the number of nodes, and Delta is the maximum node degree. Using the probabilistic layer, we prove a bound of O((D + log(n/epsilon)) log(Delta)), which matches the best previously-known bound for single-message broadcast over the physical network model. For multi-message broadcast, we obtain bounds of O((D + k Delta) log(n/epsilon) log(Delta)) using the basic layer and O((D + k Delta log(n/epsilon)) log(Delta)) using the probabilistic layer, for the time to deliver a message everywhere in the presence of at most k concurrent messages. Wed, 23 Feb 2011 00:00:00 GMT https://hdl.handle.net/1721.1/61391 2011-02-23T00:00:00Z https://hdl.handle.net/1721.1/57577 The Abstract MAC Layer Kuhn, Fabian; Lynch, Nancy; Newport, Calvin A diversity of possible communication assumptions complicates the study of algorithms and lower bounds for radio networks. We address this problem by defining an abstract MAC layer. This service provides reliable local broadcast communication, with timing guarantees stated in terms of a collection of abstract delay functions applied to the relevant contention. Algorithm designers can analyze their algorithms in terms of these functions, independently of specific channel behavior. Concrete implementations of the abstract MAC Layer over basic radio network models generate concrete definitions for these delay functions, automatically adapting bounds proven for the abstract service to bounds for the specific radio network under consideration. To illustrate this approach, we use the abstract MAC Layer to study the new problem of Multi-Message Broadcast, a generalization of standard single-message broadcast in which multiple messages can originate at different times and locations in the network. We present and analyze two algorithms for Multi-Message Broadcast in static networks: a simple greedy algorithm and one that uses regional leaders. We then indicate how these results can be extended to mobile networks. Thu, 26 Aug 2010 00:00:00 GMT https://hdl.handle.net/1721.1/57577 2010-08-26T00:00:00Z https://hdl.handle.net/1721.1/57473 MAC Design for Analog Network Coding Khabbazian, Majid; Kuhn, Fabian; Lynch, Nancy; Medard, Muriel; ParandehGheibi, Ali Most medium access control mechanisms discard collided packets and consider interference harmful. Recent work on Analog Network Coding (ANC) suggests a different approach, in which multiple interfering transmissions are strategically scheduled. The received collisions are collected and then used in a decoding process, such as the ZigZag decoding process, where the packets involved in the collisions are extracted. In this paper, we present an algebraic representation of collisions and describe a general approach to recovering collisions using ANC. To study the eect of using ANC on the performance of MAC layers, we develop an ANC-based algorithm that implements an abstract MAC layer service, as defined in [1, 2], and analyze its performance. This study proves that ANC can significantly improve the performance of MAC layer services, in terms of probabilistic time guarantees for packet delivery. We illustrate how this improvement at the MAC layer can translate into faster higher-level algorithms, by analyzing the time complexity of a multiple-message network-wide broadcast algorithm that uses our ANC-based MAC service. Mon, 02 Aug 2010 00:00:00 GMT https://hdl.handle.net/1721.1/57473 2010-08-02T00:00:00Z https://hdl.handle.net/1721.1/55721 Broadcasting in Unreliable Radio Networks Oshman, Rotem; Richa, Andrea; Newport, Calvin; Lynch, Nancy; Kuhn, Fabian Practitioners agree that unreliable links, which fluctuate between working and not working, are an important characteristic of wireless networks. In contrast, most theoretical models of radio networks fix a static set of links and assume that these links work reliably throughout an execution. This gap between theory and practice motivates us to investigate how unreliable links affect theoretical bounds on broadcast in radio networks. To that end we consider a model that includes two types of links: reliable links, which always deliver messages, and unreliable links, which sometimes deliver messages and sometimes do not. It is assumed that the graph induced by the reliable links is connected, and unreliable links are controlled by a worst-case adversary. In the new model we show an(n log n) lower bound on deterministic broadcast in undirected graphs, even when all processes are initially awake and have collision detection, and an (n) lower bound on randomized broadcast in undirected networks of constant diameter. This clearly separates the new model from the classical, reliable model. On the positive side, we give two algorithms that tolerate the inherent unreliability: an O(n3=2plog n)-time deterministic algorithm and a randomized algorithm which terminates in O(n log2 n) rounds with high probability. Tue, 08 Jun 2010 00:00:00 GMT https://hdl.handle.net/1721.1/55721 2010-06-08T00:00:00Z https://hdl.handle.net/1721.1/51667 The Cost of Global Broadcast Using Abstract MAC Layers Lynch, Nancy; Kuhn, Fabian; Kowalski, Dariusz; Khabbazian, Majid We analyze greedy algorithms for broadcasting messages throughout a multi-hop wireless network, using a slot-based model that includes message collisions without collision detection. Our algorithms are split formally into two pieces: a high-level piece for broadcast and a low-level piece for contention management. We accomplish the split using abstract versions of the MAC layer to encapsulate the contention management. We use two different abstract MAC layers: a basic non-probabilistic one, which our contention management algorithm implements with high probability, and a probabilistic one, which our contention management algorithm implements precisely. Using this approach, we obtain the following complexity bounds: Single-message broadcast, using the basic abstract MAC layer, takes time O(D log(n/epsilon) log(Delta)) to deliver the message everywhere with probability 1 - epsilon, where D is the network diameter, n is the number of nodes, and Delta is the maximum node degree. Single-message broadcast, using the probabilistic abstract MAC layer, takes time only O((D + log(n/epsilon)) log(Delta)). For multi-message broadcast, the bounds are O((D + k' Delta) log(n/epsilon) log(Delta)) using the basic layer and O((D + k' Delta log(n/epsilon)) log(Delta)) using the probabilistic layer,for the time to deliver a single message everywhere in the presence of at most k' concurrent messages. Tue, 09 Feb 2010 00:00:00 GMT https://hdl.handle.net/1721.1/51667 2010-02-09T00:00:00Z https://hdl.handle.net/1721.1/49814 Distributed Computation in Dynamic Networks Oshman, Rotem; Lynch, Nancy; Kuhn, Fabian In this report we investigate distributed computation in dynamic networks in which the network topology changes from round to round. We consider a worst-case model in which the communication links for each round are chosen by an adversary, and nodes do not know who their neighbors for the current round are before they broadcast their messages. The model is intended to capture mobile networks and wireless networks, in which mobility and interference render communication unpredictable. The model allows the study of the fundamental computation power of dynamic networks. In particular, it captures mobile networks and wireless networks, in which mobility and interference render communication unpredictable. In contrast to much of the existing work on dynamic networks, we do not assume that the network eventually stops changing; we require correctness and termination even in networks that change continually. We introduce a stability property called T-interval connectivity (for T >= 1), which stipulates that for every T consecutive rounds there exists a stable connected spanning subgraph. For T = 1 this means that the graph is connected in every round, but changes arbitrarily between rounds. Algorithms for the dynamic graph model must cope with these unceasing changes. We show that in 1-interval connected graphs it is possible for nodes to determine the size of the network and compute any computable function of their initial inputs in O(n^2) rounds using messages of size O(log n + d), where d is the size of the input to a single node. Further, if the graph is T-interval connected for T > 1, the computation can be sped up by a factor of T, and any function can be computed in O(n + n^2 / T) rounds using messages of size O(log n + d). We also give two lower bounds on the gossip problem, which requires the nodes to disseminate k pieces of information to all the nodes in the network. We show an Omega(n log k) bound on gossip in 1-interval connected graphs against centralized algorithms, and an Omega(n + nk / T) bound on exchanging k pieces of information in T-interval connected graphs for a restricted class of randomized distributed algorithms. The T-interval connected dynamic graph model is a novel model, which we believe opens new avenues for research in the theory of distributed computing in wireless, mobile and dynamic networks. Tue, 10 Nov 2009 00:00:00 GMT https://hdl.handle.net/1721.1/49814 2009-11-10T00:00:00Z https://hdl.handle.net/1721.1/45553 Modeling Radio Networks Lynch, Nancy; Newport, Calvin We describe a modeling framework and collection of foundational composition results for the study of probabilistic distributed algorithms in synchronous radio networks. Existing results in this setting rely on informal descriptions of the channel behavior and therefore lack easy comparability and are prone to error caused by definition subtleties. Our framework rectifies these issues by providing: (1) a method to precisely describe a radio channel as a probabilistic automaton; (2) a mathematical notion of implementing one channel using another channel, allowing for direct comparisons of channel strengths and a natural decomposition of problems into implementing a more powerful channel and solving the problem on the powerful channel; (3) a mathematical definition of a problem and solving a problem; (4) a pair of composition results that simplify the tasks of proving properties about channel implementation algorithms and combining problems with channel implementations. Our goal is to produce a model streamlined for the needs of the radio network algorithms community. Thu, 04 Jun 2009 00:00:00 GMT https://hdl.handle.net/1721.1/45553 2009-06-04T00:00:00Z https://hdl.handle.net/1721.1/45515 The Abstract MAC Layer Kuhn, Fabian; Newport, Calvin; Lynch, Nancy A diversity of possible communication assumptions complicates the study of algorithms and lower bounds for radio networks. We address this problem by defining an Abstract MAC Layer. This service provides reliable local broadcast communication, with timing guarantees stated in terms of a collection of abstract \emph{delay functions} applied to the relevant contention. Algorithm designers can analyze their algorithms in terms of these functions, independently of specific channel behavior. Concrete implementations of the Abstract MAC Layer over basic radio network models generate concrete definitions for these delay functions, automatically adapting bounds proven for the abstract service to bounds for the specific radio network under consideration. To illustrate this approach, we use the Abstract MAC Layer to study the new problem of Multi-Message Broadcast, a generalization of standard single-message broadcast, in which any number of messages arrive at any processes at any times.We present and analyze two algorithms for Multi-Message Broadcast in static networks: a simple greedy algorithm and one that uses regional leaders. We then indicate how these results can be extended to mobile networks. Mon, 11 May 2009 00:00:00 GMT https://hdl.handle.net/1721.1/45515 2009-05-11T00:00:00Z https://hdl.handle.net/1721.1/44516 Self-Stabilizing Message Routing in Mobile ad hoc Networks Lynch, Nancy; Lahiani, Limor; Dolev, Shlomi; Nolte, Tina We present a self-stabilizing algorithm for routing messages between arbitrary pairs of nodes in a mobile ad hoc network. Our algorithm assumes the availability of a reliable GPS service, which supplies mobile nodes with accurate information about real time and about their own geographical locations. The GPS service provides an external, shared source of consistency for mobile nodes, allowing them to label and timestamp messages, and thereby aiding in recovery from failures. Our algorithm utilizes a Virtual Infrastructure programming abstraction layer, consisting of mobile client nodes, virtual stationary timed machines called Virtual Stationary Automata (VSAs), and a local broadcast service connecting VSAs and mobile clients. VSAs are associated with predetermined regions in the plane, and are emulated in a self-stabilizing manner by the mobile nodes. VSAs are relatively stable in the face of node mobility and failure, and can be used to simplify algorithm development for mobile networks. Our routing algorithm consists of three subalgorithms: [(1)] a VSA-to-VSA geographical routing algorithm, [2] a mobile client location management algorithm, and [3] the main algorithm, which utilizes both location management and geographical routing. All three subalgorithms are self-stabilizing, and consequently, the entire algorithm is also self-stabilizing. Wed, 28 Jan 2009 00:00:00 GMT https://hdl.handle.net/1721.1/44516 2009-01-28T00:00:00Z https://hdl.handle.net/1721.1/43711 Modeling Computational Security in Long-Lived Systems, Version 2 Lynch, Nancy; Pereira, Olivier; Kaynar, Dilsun; Cheung, Ling; Canetti, Ran For many cryptographic protocols, security relies on the assumption that adversarial entities have limited computational power. This type of security degrades progressively over the lifetime of a protocol. However, some cryptographic services, such as timestamping services or digital archives, are long-lived in nature; they are expected to be secure and operational for a very long time (i.e., super-polynomial). In such cases, security cannot be guaranteed in the traditional sense: a computationally secure protocol may become insecure if the attacker has a super-polynomial number of interactions with the protocol. This paper proposes a new paradigm for the analysis of long-lived security protocols. We allow entities to be active for a potentially unbounded amount of real time, provided they perform only a polynomial amount of work per unit of real time. Moreover, the space used by these entities is allocated dynamically and must be polynomially bounded. We propose a new notion of long-term implementation, which is an adaptation of computational indistinguishability to the long-lived setting. We show that long-term implementation is preserved under polynomial parallel composition and exponential sequential composition. We illustrate the use of this new paradigm by analyzing some security properties of the long-lived timestamping protocol of Haber and Kamat. Sat, 22 Nov 2008 00:00:00 GMT https://hdl.handle.net/1721.1/43711 2008-11-22T00:00:00Z https://hdl.handle.net/1721.1/35918 Using Task-Structured Probabilistic I/O Automata to Analyze an Oblivious Transfer Protocol Canetti, Ran; Cheung, Ling; Kaynar, Dilsun; Liskov, Moses; Lynch, Nancy; Pereira, Olivier; Segala, Roberto The Probabilistic I/O Automata framework of Lynch, Segala and Vaandrager provides tools for precisely specifying protocols and reasoning about their correctness using multiple levels of abstraction, based on implementation relationships between these levels. We enhance this framework to allow analyzing protocols that use cryptographic primitives. This requires resolving and reconciling issues such as nondeterministic behavior and scheduling, randomness, resource-bounded computation, and computational hardness assumptions. The enhanced framework allows for more rigorous and systematic analysis of cryptographic protocols. To demonstrate the use of this framework, we present an example analysis that we have done for an Oblivious Transfer protocol. Fri, 16 Feb 2007 00:00:00 GMT https://hdl.handle.net/1721.1/35918 2007-02-16T00:00:00Z https://hdl.handle.net/1721.1/33964 Task-Structured Probabilistic I/O Automata Canetti,, Ran; Cheung,, Ling; Kaynar,, Dilsun; Liskov,, Moses; Lynch,, Nancy; Pereira,, Olivier; Segala, Roberto Modeling frameworks such as Probabilistic I/O Automata (PIOA) andMarkov Decision Processes permit both probabilistic andnondeterministic choices. In order to use such frameworks to express claims about probabilities of events, one needs mechanisms for resolving nondeterministic choices. For PIOAs, nondeterministic choices have traditionally been resolved by schedulers that have perfect information about the past execution. However, such schedulers are too powerful for certain settings, such as cryptographic protocol analysis, where information must sometimes be hidden. Here, we propose a new, less powerful nondeterminism-resolutionmechanism for PIOAs, consisting of tasks and local schedulers.Tasks are equivalence classes of system actions that are scheduled byoblivious, global task sequences. Local schedulers resolve nondeterminism within system components, based on local information only. The resulting task-PIOA framework yields simple notions of external behavior and implementation, and supports simple compositionality results.We also define a new kind of simulation relation, and show it to besound for proving implementation. We illustrate the potential of the task-PIOA framework by outlining its use in verifying an Oblivious Transfer protocol. Tue, 05 Sep 2006 00:00:00 GMT https://hdl.handle.net/1721.1/33964 2006-09-05T00:00:00Z https://hdl.handle.net/1721.1/33217 Using Task-Structured Probabilistic I/O Automata to Analyze an Oblivious Transfer Protocol Canetti, Ran; Cheung, Ling; Kaynar, Dilsun; Liskov, Moses; Lynch, Nancy; Pereira, Olivier; Segala, Roberto The Probabilistic I/O Automata framework of Lynch, Segala and Vaandrager provides tools for precisely specifying protocols and reasoning about theircorrectness using multiple levels of abstraction, based on implementation relationships between these levels. We enhance this framework to allow analyzingprotocols that use cryptographic primitives. This requires resolving andreconciling issues such as nondeterministic behavior and scheduling, randomness,resource-bounded computation, and computational hardness assumptions. The enhanced framework allows for more rigorous and systematic analysis of cryptographic protocols. To demonstrate the use of this framework, we present an example analysis that we have done for an Oblivious Transfer protocol. Tue, 20 Jun 2006 00:00:00 GMT https://hdl.handle.net/1721.1/33217 2006-06-20T00:00:00Z https://hdl.handle.net/1721.1/33154 Using Probabilistic I/O Automata to Analyze an Oblivious Transfer Protocol Canetti, Ran; Cheung, Ling; Kaynar, Dilsun; Liskov, Moses; Lynch, Nancy; Pereira, Olivier; Segala, Roberto We demonstrate how to carry out cryptographic security analysis ofdistributed protocols within the Probabilistic I/O Automataframework of Lynch, Segala, and Vaandrager. This framework providestools for arguing rigorously about the concurrency and schedulingaspects of protocols, and about protocols presented at differentlevels of abstraction. Consequently, it can help in makingcryptographic analysis more precise and less susceptible to errors.We concentrate on a relatively simple two-party Oblivious Transferprotocol, in the presence of a semi-honest adversary (essentially,an eavesdropper). For the underlying cryptographic notion ofsecurity, we use a version of Canetti's Universally Composablesecurity.In spite of the relative simplicity of the example, the exercise isquite nontrivial. It requires taking many fundamental issues intoaccount, including nondeterministic behavior, scheduling,resource-bounded computation, and computational hardness assumptionsfor cryptographic primitives. Mon, 19 Jun 2006 00:00:00 GMT https://hdl.handle.net/1721.1/33154 2006-06-19T00:00:00Z https://hdl.handle.net/1721.1/32525 Task-Structured Probabilistic I/O Automata Canetti, Ran; Cheung, Ling; Kaynar, Dilsun; Liskov, Moses; Lynch, Nancy; Pereira, Olivier; Segala, Roberto In the Probabilistic I/O Automata (PIOA) framework, nondeterministicchoices are resolved using perfect-information schedulers,which are similar to history-dependent policies for Markov decision processes(MDPs). These schedulers are too powerful in the setting of securityanalysis, leading to unrealistic adversarial behaviors. Therefore, weintroduce in this paper a novel mechanism of task partitions for PIOAs.This allows us to define partial-information adversaries in a systematicmanner, namely, via sequences of tasks.The resulting task-PIOA framework comes with simple notions of externalbehavior and implementation, and supports simple compositionalityresults. A new type of simulation relation is defined and proven soundwith respect to our notion of implementation. To illustrate the potentialof this framework, we summarize our verification of an ObliviousTransfer protocol, where we combine formal and computational analyses.Finally, we present an extension with extra expressive power, usinglocal schedulers of individual components. Fri, 31 Mar 2006 00:00:00 GMT https://hdl.handle.net/1721.1/32525 2006-03-31T00:00:00Z https://hdl.handle.net/1721.1/31310 Using Task-Structured Probabilistic I/O Automata to Analyze an Oblivious Transfer Protocol Canetti, Ran; Cheung, Ling; Kaynar, Dilsun; Liskov, Moses; Lynch, Nancy; Pereira, Olivier; Segala, Roberto AbstractThe Probabilistic I/O Automata framework of Lynch, Segala and Vaandrager provides tools for precisely specifying protocols and reasoning about their correctness using multiple levels of abstraction, based on implementation relationships between these levels. We enhance this framework to allow analyzing protocols that use cryptographic primitives. This requires resolving and reconciling issues such as nondeterministic behavior and scheduling, randomness, resource-bounded computation, and computational hardness assumptions. The enhanced framework allows for more rigorous and systematic analysis of cryptographic protocols. To demonstrate the use of this framework, wepresent an example analysis that we have done for an Oblivious Transfer protocol. Wed, 08 Mar 2006 00:00:00 GMT https://hdl.handle.net/1721.1/31310 2006-03-08T00:00:00Z https://hdl.handle.net/1721.1/30566 Using Probabilistic I/O Automata to Analyze an Oblivious Transfer Protocol Canetti, Ran; Cheung, Ling; Kaynar, Dilsun; Liskov, Moses; Lynch, Nancy; Olivier; Segala, Roberto We demonstrate how to carry out cryptographic security analysis ofdistributed protocols within the Probabilistic I/O Automata frameworkof Lynch, Segala, and Vaandrager.This framework provides tools for arguing rigorously about theconcurrency and scheduling aspects of protocols, and about protocolspresented at different levels of abstraction.Consequently, it can help in making cryptographic analysis moreprecise and less susceptible to errors.We concentrate on a relatively simple two-party Oblivious Transferprotocol, in the presence of a semi-honest adversary (essentially, aneavesdropper).For the underlying cryptographic notion of security, we use a versionof Canetti's Universally Composable security.In spite of the relative simplicity of the example, the exercise isquite nontrivial.It requires taking many fundamental issues into account,including nondeterministic behavior, scheduling, resource-boundedcomputation, and computational hardness assumptions for cryptographicprimitives. Fri, 19 Aug 2005 00:00:00 GMT https://hdl.handle.net/1721.1/30566 2005-08-19T00:00:00Z https://hdl.handle.net/1721.1/30563 Self-Stabilizing Mobile Node Location Management and Message Dolev, Shlomi; Lahiani, Limor; Lynch, Nancy; Nolte, Tina We present simple algorithms for achieving self-stabilizing locationmanagement and routing in mobile ad-hoc networks. While mobile clients maybe susceptible to corruption and stopping failures, mobile networks areoften deployed with a reliable GPS oracle, supplying frequent updates ofaccurate real time and location information to mobile nodes. Informationfrom a GPS oracle provides an external, shared source of consistency formobile nodes, allowing them to label and timestamp messages, and henceaiding in identification of, and eventual recovery from, corruption andfailures. Our algorithms use a GPS oracle.Our algorithms also take advantage of the Virtual Stationary Automataprogramming abstraction, consisting of mobile clients, virtual timedmachines called virtual stationary automata (VSAs), and a local broadcastservice connecting VSAs and mobile clients. VSAs are distributed at knownlocations over the plane, and emulated in a self-stabilizing manner by themobile nodes in the system. They serve as fault-tolerant building blocksthat can interact with mobile clients and each other, and can simplifyimplementations of services in mobile networks.We implement three self-stabilizing, fault-tolerant services, each builton the prior services: (1) VSA-to-VSA geographic routing, (2) mobileclient location management, and (3) mobile client end-to-end routing. Weuse a greedy version of the classical depth-first search algorithm toroute messages between VSAs in different regions. The mobile clientlocation management service is based on home locations: Each clientidentifier hashes to a set of home locations, regions whose VSAs areperiodically updated with the client\'s location. VSAs maintain thisinformation and answer queries for client locations. Finally, theVSA-to-VSA routing and location management services are used to implementmobile client end-to-end routing. Thu, 11 Aug 2005 00:00:00 GMT https://hdl.handle.net/1721.1/30563 2005-08-11T00:00:00Z https://hdl.handle.net/1721.1/30535 Motion Coordination Using Virtual Nodes Lynch, Nancy; Mitra, Sayan; Nolte, Tina We describe how a virtual node abstraction layer can be used to coordinate the motion of real mobile nodes in a region of 2-space. In particular, we consider how nodes in a mobile ad hoc network can arrange themselves along a predetermined curve in the plane, and can maintain themselves in such a configuration in the presence of changes in the underlying mobile ad hoc network, specifically, when nodes may join or leave the system or may fail. Our strategy is to allow the mobile nodes to implement a virtual layer consisting of mobile client nodes, stationary Virtual Nodes (VNs) for predetermined zones in the plane, and local broadcast communication. The VNs coordinate among themselves to distribute the client nodesbetween zones based on the length of the curve through those zones, while each VN directs its zone's local client nodes to move themselves to equally spaced locations on the local portion of the target curve. Wed, 06 Apr 2005 00:00:00 GMT https://hdl.handle.net/1721.1/30535 2005-04-06T00:00:00Z https://hdl.handle.net/1721.1/30526 Impossibility of boosting distributed service resilience Attie, Paul; Guerraoui, Rachid; Kouznetsov, Petr; Lynch, Nancy; Rajsbaum, Sergio We prove two theorems saying that no distributed system in whichprocesses coordinate using reliable registers and f-resilient servicescan solve the consensus problem in the presence of f+1 undetectableprocess stopping failures. (A service is f-resilient if it isguaranteed to operate as long as no more than f of the processesconnected to it fail.)Our first theorem assumes that the given services are atomic objects,and allows any connection pattern between processes and services. Incontrast, we show that it is possible to boost the resilience ofsystems solving problems easier than consensus: the k-set consensusproblem is solvable for 2k-1 failures using 1-resilient consensusservices. The first theorem and its proof generalize to the largerclass of failure-oblivious services.Our second theorem allows the system to contain failure-awareservices, such as failure detectors, in addition to failure-obliviousservices; however, it requires that each failure-aware service beconnected to all processes. Thus, f+1 process failures overall candisable all the failure-aware services. In contrast, it is possibleto boost the resilience of a system solving consensus if arbitrarypatterns of connectivity are allowed between processes andfailure-aware services: consensus is solvable for any number offailures using only 1-resilient 2-process perfect failure detectors. Fri, 25 Feb 2005 00:00:00 GMT https://hdl.handle.net/1721.1/30526 2005-02-25T00:00:00Z https://hdl.handle.net/1721.1/30486 Systematic Removal of Nondeterminism for Code Generation in I/O Automata Vaziri, Mandana; Tauber, Joshua A.; Tsai, Michael J.; Lynch, Nancy The Input/Output (I/O) automaton model developed by Lynch and Tuttle models components in asynchronous concurrentsystems as labeled transition systems. IOA is a precise language for describing I/O automata and for stating their properties. A toolset is beingdeveloped for IOA to support distributed software design and implementation. One of the tools consists of a userassisted code generator fromIOA into an imperative programming language such as C or Java. One aspect that distinguishes IOA programs from programs written inimperative languages is the presence of nondeterminism which comesin the form of explicit nondeterministic statements and implicit scheduling choices made during execution. Code generation therefore consistspartially of systematically removing all forms of nondeterminism. In this paper, we describe our approach and design for code generation.We focus on the issue of removing implicit nondeterminism and specify a transformation on IOA programs that makes all nondeterminismexplicit. The programmer can then replace all explicit nondeterminismwith deterministic statements prior to code generation. We also describethis transformation at a semantic level i.e., at the level of the I/O automaton mathematical model. We show that the transformation definedat the IOA level conforms to the one at the semantic level. Mon, 19 Jul 2004 00:00:00 GMT https://hdl.handle.net/1721.1/30486 2004-07-19T00:00:00Z https://hdl.handle.net/1721.1/30450 Virtual Mobile Nodes for Mobile Ad Hoc Networks Dolev, Shlomi; Gilbert, Seth; Lynch, Nancy A.; Schiller, Elad; Shvarstman, Alex A.; Welch, Jennifer One of the most significant challenges introduced by mobile networks is the difficulty in coping withthe unpredictable movement of mobile nodes. If, instead, the mobile nodes could be programmed totravel through the world in a predictable and useful manner, the task of designing algorithms for mobilenetworks would be significantly simplified. Alas, users of mobile devices in the real world are notamenable to following instructions as to where their devices may travel.While real mobile nodes may be disinclined to move as desired, we propose executing algorithmson virtual mobile nodes that move in a predetermined, predictable, manner through the real world. Inthis paper, we define the Virtual Mobile Node Abstraction, and present selected algorithms that takeadvantage of virtual mobile nodes to simply and efficiently perform complicated tasks in highly dynamic,unpredictable mobile ad hoc networks.We then present the Mobile Point Emulator, a new algorithm that implements robust virtual mobilenodes. This algorithm replicates the virtual node at a constantly changing set of real nodes, choosingnew replicas as the real nodes move in and out of the path of the virtual node. We claim that the MobilePoint algorithm correctly implements a virtual mobile node, and that it is robust as long as the virtualnode travels through well-populated areas of the network. Thu, 26 Feb 2004 00:00:00 GMT https://hdl.handle.net/1721.1/30450 2004-02-26T00:00:00Z https://hdl.handle.net/1721.1/30449 GeoQuorums: Implementing Atomic Memory in Mobile Ad Hoc Networks Dolev, Shlomi; Gilbert, Seth; Lynch, Nancy A.; Shvartsman, Alex A.; Welch, Jennifer L. We present a new approach, the GeoQuorums approach, for implementing atomic read/write shared memoryin mobile ad hoc networks. Our approach is based on associating abstract atomic objects with certain geographiclocations. We assume the existence of focal points, geographic areas that are normally “populated” by mobile nodes.For example, a focal point may be a road junction, a scenic observation point, or a water resource in the desert. Mobilenodes that happen to populate a focal point participate in implementing a shared atomic object, using a replicated statemachine approach. These objects, which we call focal point objects, are then used to implement atomic read/writeoperations on a virtual shared object, using our new GeoQuorums algorithm. The GeoQuorums algorithm uses aquorum-based strategy in which each each quorum consists of a set of focal point objects. The quorums are used tomaintain the consistency of the shared memory and to tolerate limited failures of the focal point objects, caused bydepopulation of the corresponding geographic areas. We present a mechanism for changing the set of quorums onthe fly, thus improving efficiency. Overall, the new GeoQuorums algorithm efficiently implements read and writeoperations in a highly dynamic, mobile network. Wed, 25 Feb 2004 00:00:00 GMT https://hdl.handle.net/1721.1/30449 2004-02-25T00:00:00Z https://hdl.handle.net/1721.1/30448 MultiChord: A Resilient Namespace Management Protocol Lynch, Nancy; Stoica, Ion MultiChord is a new variant of the Chord namespace management algorithm [7] that includes lightweight mechanismsfor accommodating a limited rate of change, specifically, process joins and failures. This paper describes thealgorithm formally and evaluates its performance, using both simulation and analysis. Our main result is that lookupsare provably correct—that is, each lookup returns results that are consistent with a hypothetical ideal system that differsfrom the actual system only in entries corresponding to recent joins and failures—in the presence of a limited rateof change. In particular, if the number of joins and failures that occur during a given time interval in a given regionof system are bounded, then all lookups are correct. A second result is a guaranteed upper bound for the latency of alookup operation in the absence of any other lookups in the system. Finally, we establish a relationship between thedeterministic assumptions of bounded joins and failures and the probabilistic assumptions (which are often used tomodel large scale networks). In particular, we derive a lower bound for the mean time between two violations of thedeterministic assumptions in a steady state system where joins and failures are modeled by Poisson processes. Thu, 19 Feb 2004 00:00:00 GMT https://hdl.handle.net/1721.1/30448 2004-02-19T00:00:00Z https://hdl.handle.net/1721.1/30422 Dynamic Input/Output Automata: A Formal Model for Dynamic Systems Attie, Paul C.; Lynch, Nancy A. We present a mathematical state-machine model, the Dynamic I/O Automaton (DIOA) model, for defining and analyzing dynamic systems of interacting components. The systems we consider are dynamic in two senses: (1) components can be created and destroyed as computation proceeds, and (2) the events in which the components may participate may change. The new model admits a notion of external system behavior, based on sets of traces. It also features a parallel composition operator for dynamic systems, which respects external behavior, and a notion of simulation from one dynamic system to another, which can be used to prove that one system implements the other. Sat, 26 Jul 2003 00:00:00 GMT https://hdl.handle.net/1721.1/30422 2003-07-26T00:00:00Z https://hdl.handle.net/1721.1/30410 A Reliable Broadcast Scheme for Sensor Networks Livadas, Carolos; Lynch, Nancy A. In this short technical report, we present a simple yet effective reliable broadcast protocol for sensor networks. This protocol disseminates packets throughout the sensor network by flooding and recovers from losses resulting from collisions by having hosts retransmit packets whenever they notice that their neighbors have fallen behind. Such retransmissions serve to flood the appropriate packets throughout the regions of the sensor network that did not receive the given packets as a result of prior flooding attempts. Mon, 11 Aug 2003 00:00:00 GMT https://hdl.handle.net/1721.1/30410 2003-08-11T00:00:00Z https://hdl.handle.net/1721.1/30407 The Theory of Timed I/O Automata Kaynor, Dilsun K.; Lynch, Nancy; Segala, Roberto; Vaandrager, Frits This monograph presents the Timed Input/Output Automaton (TIOA) modeling framework, a basic mathematical framework to support description and analysis of timed systems. Wed, 02 Mar 2005 00:00:00 GMT https://hdl.handle.net/1721.1/30407 2005-03-02T00:00:00Z https://hdl.handle.net/1721.1/30403 The Theory of Timed I/O Automata Kaynar, Dilsun K.; Lynch, Nancy; Segala, Roberto; Vaandrager, Frits Revised version -- November 23, 2004.This paper presents the Timed Input/Output Automaton (TIOA) modeling framework, a basic mathematical framework to support description and analysis of timed systems. Wed, 27 Aug 2003 00:00:00 GMT https://hdl.handle.net/1721.1/30403 2003-08-27T00:00:00Z