Now showing items 1-20 of 107

    • Dynamic Input/Output Automata: A Formal Model for Dynamic Systems 

      Attie, Paul C.; Lynch, Nancy A. (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 

      Livadas, Carolos; Lynch, Nancy A. (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 

      Kaynar, Dilsun K.; Lynch, Nancy; Segala, Roberto; Vaandrager, Frits (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 

      Lynch, Nancy; Stoica, Ion (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 

      Dolev, Shlomi; Gilbert, Seth; Lynch, Nancy A.; Shvartsman, Alex A.; Welch, Jennifer L. (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 

      Dolev, Shlomi; Gilbert, Seth; Lynch, Nancy A.; Schiller, Elad; Shvarstman, Alex A.; e.a. (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 

      Vaziri, Mandana; Tauber, Joshua A.; Tsai, Michael J.; Lynch, Nancy (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 

      Attie, Paul; Guerraoui, Rachid; Kouznetsov, Petr; Lynch, Nancy; Rajsbaum, Sergio (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 

      Kaynor, Dilsun K.; Lynch, Nancy; Segala, Roberto; Vaandrager, Frits (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 

      Lynch, Nancy; Mitra, Sayan; Nolte, Tina (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 

      Dolev, Shlomi; Lahiani, Limor; Lynch, Nancy; Nolte, Tina (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 

      Canetti, Ran; Cheung, Ling; Kaynar, Dilsun; Liskov, Moses; Lynch, Nancy; e.a. (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 

      Canetti, Ran; Cheung, Ling; Kaynar, Dilsun; Liskov, Moses; Lynch, Nancy; e.a. (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 

      Canetti, Ran; Cheung, Ling; Kaynar, Dilsun; Liskov, Moses; Lynch, Nancy; e.a. (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 

      Canetti, Ran; Cheung, Ling; Kaynar, Dilsun; Liskov, Moses; Lynch, Nancy; e.a. (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 

      Canetti, Ran; Cheung, Ling; Kaynar, Dilsun; Liskov, Moses; Lynch, Nancy; e.a. (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 

      Canetti,, Ran; Cheung,, Ling; Kaynar,, Dilsun; Liskov,, Moses; Lynch,, Nancy; e.a. (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 

      Canetti, Ran; Cheung, Ling; Kaynar, Dilsun; Liskov, Moses; Lynch, Nancy; e.a. (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 

      Lynch, Nancy; Pereira, Olivier; Kaynar, Dilsun; Cheung, Ling; Canetti, Ran (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 ...
    • Brief announcement: Hardness of broadcasting in wireless networks with unreliable communication 

      Newport, Calvin Charles; Kuhn, Fabian; Lynch, Nancy Ann (Association for Computing Machinery, 2009)
      We prove two broadcast lower bounds for a wireless network model that includes unreliable links. For deterministic algorithms, we show n − 1 rounds are required, where n is the number of processes. For randomized algorithms, ...