TY - GEN
T1 - A formalized theory for verifying stability and convergence of automata in PVS
AU - Mitra, Sayan
AU - Chandy, K. Mani
N1 - Funding Information:
The work is funded in part by the Caltech Information Science and Technology Center and AFOSR MURI FA9550-06-1-0303.
PY - 2008
Y1 - 2008
N2 - 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.
AB - 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.
UR - http://www.scopus.com/inward/record.url?scp=57049177889&partnerID=8YFLogxK
UR - http://www.scopus.com/inward/citedby.url?scp=57049177889&partnerID=8YFLogxK
U2 - 10.1007/978-3-540-71067-7_20
DO - 10.1007/978-3-540-71067-7_20
M3 - Conference contribution
AN - SCOPUS:57049177889
SN - 3540710655
SN - 9783540710653
T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
SP - 230
EP - 245
BT - Theorem Proving in Higher Order Logics - 21st International Conference, TPHOLs 2008, Proceedings
PB - Springer
T2 - 21st International Conference on Theorem Proving in Higher Order Logics, TPHOLs 2008
Y2 - 18 August 2008 through 21 August 2008
ER -