Browsing Technical Reports and Memos by Issue Date
Now showing items 1-20 of 40
-
Dynamic Input/Output Automata: A Formal Model for Dynamic Systems
(2003-07-26)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 ... -
A Reliable Broadcast Scheme for Sensor Networks
(2003-08-11)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 ... -
The Theory of Timed I/O Automata
(2003-08-27)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. -
MultiChord: A Resilient Namespace Management Protocol
(2004-02-19)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 ... -
GeoQuorums: Implementing Atomic Memory in Mobile Ad Hoc Networks
(2004-02-25)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. ... -
Virtual Mobile Nodes for Mobile Ad Hoc Networks
(2004-02-26)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 ... -
Systematic Removal of Nondeterminism for Code Generation in I/O Automata
(2004-07-19)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 ... -
Impossibility of boosting distributed service resilience
(2005-02-25)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 ... -
The Theory of Timed I/O Automata
(2005-03-02)This monograph presents the Timed Input/Output Automaton (TIOA) modeling framework, a basic mathematical framework to support description and analysis of timed systems. -
Motion Coordination Using Virtual Nodes
(2005-04-06)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 ... -
Self-Stabilizing Mobile Node Location Management and Message
(2005-08-11)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 ... -
Using Probabilistic I/O Automata to Analyze an Oblivious Transfer Protocol
(2005-08-19)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 ... -
Using Task-Structured Probabilistic I/O Automata to Analyze an Oblivious Transfer Protocol
(2006-03-08)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 ... -
Task-Structured Probabilistic I/O Automata
(2006-03-31)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 ... -
Using Probabilistic I/O Automata to Analyze an Oblivious Transfer Protocol
(2006-06-19)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 ... -
Using Task-Structured Probabilistic I/O Automata to Analyze an Oblivious Transfer Protocol
(2006-06-20)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 ... -
Task-Structured Probabilistic I/O Automata
(2006-09-05)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 ... -
Using Task-Structured Probabilistic I/O Automata to Analyze an Oblivious Transfer Protocol
(2007-02-16)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 ... -
Modeling Computational Security in Long-Lived Systems, Version 2
(2008-11-22)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 ... -
Self-Stabilizing Message Routing in Mobile ad hoc Networks
(2009-01-28)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 ...
