Hybrid Systems with Finite Bisimulations
Abstract
The theory of formal verification is one of the main approaches to hybrid system analysis. A unified approach to decidability questions for verification algorithms is obtained by the construction of a bisimulation. Bisimulations are finite state quotients whose reachability properties are equivalent to those of the original infinite state hybrid system. This approach has had success in the reachability analysis of timed automata and initialized rectangular automata. In this paper, we use recent results from stratification theory, subanalytic sets, and model theory in order to extend the state-of-the-art results on the existence of bisimulations for certain classes of hybrid systems.
Document Details
- Document Type
- Technical Report
- Publication Date
- Apr 01, 1998
- Accession Number
- ADA358308
Entities
People
- G. Lafferriere
- G. Pappas
- S. Sastry
Organizations
- University of California, Berkeley