Expressing and Verifying Temporal and Structural Properties of Mobile Agents