Formations of Mobile agents with Messages Loss and Delay Research GoalMain ContributionsFormations of Spatial PattersLine-up Pattern FormationLine-up Synchronous ProtocolLine-up Protocol SimulationDeviation of AgentsDeviation Simulation Message-Passing SystemsAsynchrony and Non-DeterminismLine-Up ProtocolDeviations in Asynchronous SystemDeviation ProfileProof TechniqueTechnique for the Line-up ProblemAdvantages of the ProtocolGeneral class of ProblemsConclusions and Future WorkLine-Up Pattern FormationLimitations of synchronous proofsCommunication ModelSOCAL Workshop 2008 1California Institute of TechnologyFormations of Mobile agents with Messages Loss and DelayConcetta PilottoSayan MitraK. Mani ChandySOCAL Workshop 2008 2California Institute of TechnologyResearch Goal• Arbitrary delay for channels and processors• Generally non deterministicDistributed Control Distributed Computing• Encompassing theory:∑−=∂∂kjkjxxctx)(• Synchronous steps• Instantaneous communication• Generally deterministicSOCAL Workshop 2008 3California Institute of TechnologyMain Contributions•Use of Temporal Logic to prove convergence in continuous time systems • Class of Problems: Pattern formation– Agents move in Euclidean space– Smaller and smaller adjustments to the position but never terminate• Communication model: Asynchronous message passing with loss, reordering, and delaySOCAL Workshop 2008 4California Institute of TechnologyFormations of Spatial Patters• Distributed Control:– Robots are deployed over some area– Apply very simple local protocolto update their positions synchronously– Goal: Converge to a target global configuration• Proofs of convergence: using eigen values of the transition matrixSOCAL Workshop 2008 5California Institute of TechnologyLine-up Pattern Formation• N + 1 agents with unique indices in [0,N] and common coordinate system• Ideal position predicate: Equidistance on a straight lineNixNiNxxNixxNiN**0***0}1,,1{,,+−=−∈∀ℜ∈∀ K012 3 45SOCAL Workshop 2008 6California Institute of TechnologyLine-up Synchronous Protocol• Starting from any initial configuration• Applying infinitely often⎪⎪⎩⎪⎪⎨⎧=<<+==++−NixNitxtxixtxNiii if 0 if 2)()(0 if )1(110• Agents converge to the ideal positions: equidistance points on the line between x0and xN10423tt+1t-1SOCAL Workshop 2008 7California Institute of TechnologyLine-up Protocol SimulationSOCAL Workshop 2008 8California Institute of TechnologyDeviation of Agents• Distance between the agent’s current location from its ideal location012345Current012 3 45IdealSOCAL Workshop 2008 9California Institute of TechnologyDeviation SimulationSOCAL Workshop 2008 10California Institute of TechnologyMessage-Passing Systems• Robots are not synchronized • Robots are not able to access the state of other robots• Realistic communication model: Message-passing– Messages may be: lost, delayed (delivered in bounded time), or reordered• Hence, messages may contain old information• Goal: systematic way for proving convergence by combining invariance assertions with temporal logicSOCAL Workshop 2008 11California Institute of TechnologyAsynchrony and Non-Determinism• Asynchrony, message delays and losses lead to a non-deterministic system2123mm213mm• Agents 1, 3 update their states with an old value of the state of agent 2!• Can collections of agents form stable patters when each agent updates its state using the state of other agents at some unknown time in the past?SOCAL Workshop 2008 12California Institute of Technology• Agents broadcast their state (position) infinitely often– Communication based on indices rather than distances• Messages:– can be lost or delivered in bounded but unknown time– Weak assumption: Delivery of some messages to agent i from at least one of the other agentsCommunication ModelSOCAL Workshop 2008 13California Institute of TechnologyLine-Up ProtocolAgent i performs the following tasks:(1) Periodically broadcasts messages containing its target position xti(2) Upon receiving a message from a lower agent l and higher r computes its new target position:(3) Moves toward the target position xtixllrirxrlrlixti−−+−−=alaiaraiWeighted-Average of al and arxliiiixriiiixti)1()1()1()1()1()1(−−+−++−−+−−=SOCAL Workshop 2008 14California Institute of TechnologyDeviations in Asynchronous System• Distance between the agent’s current location from its ideal location• Max Deviation:– Messages in the channels ⇒ in the same state several positions associated with the same agent (state variables and messages in transit) ⇒ take the max of these!SOCAL Workshop 2008 15California Institute of TechnologyDeviation Profile N][0,j∈∀• Left profile: L(s)01234 5Max DeviationLeft Profile⎟⎠⎞⎜⎝⎛−≤− jNssj211)max(),(max_dev⎟⎠⎞⎜⎝⎛−≤jssj211)max(),(max_dev• Right profile: R(s) N][0,j∈∀SOCAL Workshop 2008 16California Institute of TechnologyProof Technique• Safety: f: States → R })({ })({ ksfksfaa≤′⎯→⎯≤∀• Progress:)( kfstablek≤∀kf≤ 10 })({ })({ <≤≤′⎯→⎯≤∃kkaksfksfaααSOCAL Workshop 2008 17California Institute of TechnologyTechnique for the Line-up Problem• Profile Invariant: convex combination• Profile Decrease: eventual time-bounded delivery of messageskf≤01234 5Max DeviationLeft ProfileRight ProfileSOCAL Workshop 2008 18California Institute of TechnologyAdvantages of the Protocol• Agent i– only the relative rank of r and l: (i - l) and (r – i)– Does not know the total number of agents012 3 45012 3 4 5012345• Robustness: Work even if – some agents fail– Set of agents is partitioned012345SOCAL Workshop 2008 19California Institute of TechnologyGeneral class of Problems• Lines, triangles, quadrilaterals and generalization to 3 and higher dimensions• Indices of the agents are a d-dimensional tuple• Agent (i, j) can communicate with any agent with the same i or jSOCAL Workshop 2008 20California Institute of TechnologyConclusions and Future Work• Took a step towards integrating distributed control and distributed computing: – pattern formation with mobile agents• Future: Develop theorem-prover based framework for verifying mobile agent systems• Model the dynamics of the motion of the agentsSOCAL Workshop 2008 21California Institute of TechnologySOCAL Workshop 2008 22California Institute of TechnologyLine-Up Pattern Formation•