Michael S. Branicky, Ekaterina Dolginova and Nancy Lynch. A Toolbox for Proving and Maintaining Hybrid Specifications. Published in Springer Verlag Lecture Notes in Computer Science series. Presented at HS'96: Hybrid Systems IV, October 12-16, 1996, Cornell University, Ithaca, NY. .pdf

Abstract:

Formal verification in computer science often takes a worst-case view towards performance and uses induction to prove specification invariants. In control theory, robust control takes a worst-case view towards performance; nominal performance proofs often use derivative information to prove invariance of specification sets. In this note, we explore a toolbox for proving (positive) invariance of state-space sets with respect to the actions of dynamical systems. The focus is on dynamical systems given by differential equations, building up to hybrid systems.


Click here for Theory of Distributed Systems group homepage.