Sciweavers

Share
TPHOL
2008
IEEE

A Formalized Theory for Verifying Stability and Convergence of Automata in PVS

8 years 9 months ago
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 [26]. 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.
Sayan Mitra, K. Mani Chandy
Added 01 Jun 2010
Updated 01 Jun 2010
Type Conference
Year 2008
Where TPHOL
Authors Sayan Mitra, K. Mani Chandy
Comments (0)
books