A Caltech Library Service

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

Mitra, Sayan and Chandy, K. Mani (2008) A Formalized Theory for Verifying Stability and Convergence of Automata in PVS. In: Theorem Proving in Higher Order Logics. Lecture Notes in Computer Science. No.5170. Springer , Berlin, pp. 230-245. ISBN 9783540710653.

Full text is not posted in this repository. Consult Related URLs below.

Use this Persistent URL to link to this item:


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.

Item Type:Book Section
Related URLs:
URLURL TypeDescription ReadCube access
Additional Information:© 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.
Funding AgencyGrant Number
Caltech Information Science and Technology (IST) InitiativeUNSPECIFIED
Air Force Office of Scientific Research (AFOSR)FA9550-06-1-0303
Subject Keywords:Distance Function; Topological Structure; Formalize Theory; Mobile Agent; Nonempty Subset
Series Name:Lecture Notes in Computer Science
Issue or Number:5170
Record Number:CaltechAUTHORS:20180809-133557629
Persistent URL:
Usage Policy:No commercial reproduction, distribution, display or performance rights in this work are provided.
ID Code:88705
Deposited By: George Porter
Deposited On:09 Aug 2018 21:28
Last Modified:16 Nov 2021 00:29

Repository Staff Only: item control page