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. https://resolver.caltech.edu/CaltechAUTHORS:20180809-133557629
Full text is not posted in this repository. Consult Related URLs below.
Use this Persistent URL to link to this item: https://resolver.caltech.edu/CaltechAUTHORS:20180809-133557629
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.
| Item Type: | Book Section | |||||||||
|---|---|---|---|---|---|---|---|---|---|---|
| Related URLs: |
| |||||||||
| 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. | |||||||||
| Funders: |
| |||||||||
| Subject Keywords: | Distance Function; Topological Structure; Formalize Theory; Mobile Agent; Nonempty Subset | |||||||||
| Series Name: | Lecture Notes in Computer Science | |||||||||
| Issue or Number: | 5170 | |||||||||
| DOI: | 10.1007/978-3-540-71067-7_20 | |||||||||
| Record Number: | CaltechAUTHORS:20180809-133557629 | |||||||||
| Persistent URL: | https://resolver.caltech.edu/CaltechAUTHORS:20180809-133557629 | |||||||||
| Usage Policy: | No commercial reproduction, distribution, display or performance rights in this work are provided. | |||||||||
| ID Code: | 88705 | |||||||||
| Collection: | CaltechAUTHORS | |||||||||
| Deposited By: | George Porter | |||||||||
| Deposited On: | 09 Aug 2018 21:28 | |||||||||
| Last Modified: | 16 Nov 2021 00:29 |
Repository Staff Only: item control page
