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. © 2008 Springer Berlin Heidelberg.
CITATION STYLE
Mitra, S., & Chandy, K. M. (2008). A formalized theory for verifying stability and convergence of automata in PVS. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 5170 LNCS, pp. 230–245). Springer Verlag. https://doi.org/10.1007/978-3-540-71067-7_20
Mendeley helps you to discover research relevant for your work.