Verification of Orbitally Self-Stabilizing Distributed Algorithms Using Lyapunov Functions and Poincare Maps