A Formalized Theory for Verifying Stability and Convergence of Automata in PVS
Correctness of many hybrid and distributed systems require stability and convergence guarantees. Unlike the standard induction principle for verifying invariance, a theory for verifying stability or convergence of automata is currently not available. In this paper, we formalize one such theory proposed by Tsitsiklis . We build on the existing PVS metatheory for untimed, timed, and hybrid input/output automata, and incorporate the concepts about fairness, stability, Lyapunov-like functions, and convergence. The resulting theory provides two sets of sufficient conditions, which when instantiated and verified for particular automata, guarantee convergence and stability, respectively.
© Springer-Verlag Berlin Heidelberg 2008. The work is funded in part by the Caltech Information Science and Technology Center and AFOSR MURI FA9550-06-1-0303.