@InProceedings{MitraChandy08:TPHOLS,
author="Mitra, Sayan
and Chandy, K. Mani",
editor="Mohamed, Otmane Ait
and Mu{\~{n}}oz, C{\'e}sar
and Tahar, Sofi{\`e}ne",
title="A Formalized Theory for Verifying Stability and Convergence of Automata in PVS",
booktitle="Theorem Proving in Higher Order Logics",
year="2008",
publisher="Springer Berlin Heidelberg",
address="Berlin, Heidelberg",
pages="230--245",
abstract="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 [27]. 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.",
isbn="978-3-540-71067-7"
}