# Formations of Mobile Agents with Message Loss and Delay

**View the full content.**View Full Document

0 0 12 views

**Unformatted text preview:**

Formations of Mobile agents with Messages Loss and Delay Concetta Pilotto Sayan Mitra K Mani Chandy California Institute of Technology SOCAL Workshop 2008 1 Research Goal Encompassing theory Distributed Control Distributed Computing Synchronous steps Instantaneous communication Generally deterministic Arbitrary delay for channels and processors Generally non deterministic x j t c California Institute of Technology x k xj k SOCAL Workshop 2008 2 Main 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 delay California Institute of Technology SOCAL Workshop 2008 3 Formations of Spatial Patters Distributed Control Robots are deployed over some area Apply very simple local protocol to update their positions synchronously Goal Converge to a target global configuration Proofs of convergence using eigen values of the transition matrix California Institute of Technology SOCAL Workshop 2008 4 Line up Pattern Formation N 1 agents with unique indices in 0 N and common coordinate system Ideal position predicate Equidistance on a straight line x0 x N i 1 K N 1 xi 0 California Institute of Technology 1 x0 2 N i i xN N N 3 4 SOCAL Workshop 2008 5 5 Line up Synchronous Protocol Starting from any initial configuration Applying infinitely often if i 0 x0 xi 1 t xi 1 t xi t 1 if 0 i N 2 if i N x N 0 1 2 3 4 t 1 t t 1 Agents converge to the ideal positions equidistance points on the line between x0 and xN California Institute of Technology SOCAL Workshop 2008 6 Line up Protocol Simulation California Institute of Technology SOCAL Workshop 2008 7 Deviation of Agents Distance between the agent s current location from its ideal location Current 2 Ideal California Institute of Technology 0 4 0 1 1 2 5 3 SOCAL Workshop 2008 4 3 5 8 Deviation Simulation California Institute of Technology SOCAL Workshop 2008 9 Message Passing Systems Robots are not synchronized Robots are not able to access the state of other robots Realistic communication model Messagepassing 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 logic California Institute of Technology SOCAL Workshop 2008 10 Asynchrony and Non Determinism Asynchrony message delays and losses lead to a non deterministic system 2 m 1 2 m 3 m 1 2 m 3 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 California Institute of Technology SOCAL Workshop 2008 11 Communication Model 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 agents California Institute of Technology SOCAL Workshop 2008 12 Line Up Protocol ai ar Agent i performs the following tasks 1 Periodically broadcasts messages containing its target position xti ai al 2 Upon receiving a message from a lower agent l and higher r computes its new target position Weighted Average of al and ar i l r i xti xr xl r l r l i i 1 xti xr i 1 i 1 i 1 i xl i 1 i 1 3 Moves toward the target position xti California Institute of Technology SOCAL Workshop 2008 13 Deviations 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 California Institute of Technology SOCAL Workshop 2008 14 Deviation Profile Left profile L s j 0 N 1 max dev j s max s 1 j 2 Right profile R s Max Deviation Left Profile 0 1 2 3 4 5 j 0 N 1 max dev j s max s 1 N j 2 California Institute of Technology SOCAL Workshop 2008 15 Proof Technique f k Safety f States R k stable f k a a f s k f s k Progress a f s k f s k k a California Institute of Technology SOCAL Workshop 2008 0 k 1 16 Max Deviation Technique for the Line up Problem Right Profile 0 1 2 Left Profile 3 4 f k 5 Profile Invariant convex combination Profile Decrease eventual time bounded delivery of messages California Institute of Technology SOCAL Workshop 2008 17 Advantages 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 agents Robustness Work even if some agents fail 0 1 Set of agents is partitioned 0 1 0 California Institute of Technology 0 1 1 2 2 3 4 2 3 4 5 2 3 5 3 SOCAL Workshop 2008 4 4 5 5 18 General 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 j California Institute of Technology SOCAL Workshop 2008 19 Conclusions 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 agents California Institute of Technology SOCAL Workshop 2008 20 California Institute of Technology SOCAL Workshop 2008 21 Line Up Pattern Formation N 1 agents with unique indices in 0 N and common coordinate system Ideal position predicate Equidistance on a straight line x0 x N i 1 K N 1 xi a0 California Institute of Technology a1 x0 N i i xN N N a2 a3 a4 SOCAL Workshop 2008 a5 22 Limitations of synchronous proofs Convergence in Synchronous Systems a1 a2 a3 a4 a5 t Updating rule Using eigenvalues of the transition matrix and Markov Chains 0 1 0 0 0 0 1 0 1 0 0 0 California Institute of Technology 0 1 0 1 0 0 0 0 1 0 1 0 0 0 0 1 0 1 0 0 0 0 1 0 1 1 0 0 0 0 1 2 1 0 0 0 0 1 2 1 0 0 0 0 1 2 1 0 0 0 0 1 2 1 0 0 0 0 1 1 SOCAL Workshop 2008 23 Communication Model m m Communication not based on distances ai a0 Channel buffer Messages a1 Buffer m m Agents broadcast their values infinitely often aN aj Incoming channel for i 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 agents