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

DOI10.1007/978-3-540-71067-7_20zbMath1165.68394OpenAlexW1502256709MaRDI QIDQ3543661

K. Mani Chandy, Sayan Mitra

Publication date: 4 December 2008

Published in: Lecture Notes in Computer Science (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/978-3-540-71067-7_20

Mathematics Subject Classification ID

Formal languages and automata (68Q45) Specification and verification (program logics, model checking, etc.) (68Q60)

Related Items (4)

On Convergence of Concurrent Systems under Regular Interactions ⋮ A formal proof in Coq of Lasalle's invariance principle ⋮ Verification of distributed systems with local-global predicates ⋮ Approximate partial order reduction

Uses Software

• PVS
• NASA PVS

Cites Work

• Switching in systems and control
• TAME: Using PVS strategies for special-purpose theorem proving
• The Theory of Timed I/O Automata, Second Edition
• Finding Lexicographic Orders for Termination Proofs in Isabelle/HOL
• On the stability of asynchronous iterative processes
• Mechanizing UNITY in Isabelle
• Formal Modeling and Analysis of Timed Systems
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item

This page was built for publication: A Formalized Theory for Verifying Stability and Convergence of Automata in PVS