Reachability analysis of hybrid systems using bisimulations

Author

Lafferriere, Gerardo ; Pappas, G.J. ; Sastry, Shankar

Author_Institution

Dept. of Math. Sci., Portland State Univ., OR, USA

Volume

2

fYear

1998

fDate

16-18 Dec 1998

Firstpage

1623

Abstract

A unified approach to decidability questions for the verification of hybrid systems is obtained by the construction of a bisimulation. These are finite state quotients whose reachability properties are equivalent to those of the original infinite state system. This approach has had some success in the reachability analysis of timed automata and linear hybrid automata. We use results from stratification theory, subanalytic sets and model theory of fields in order to extend earlier results on the existence of bisimulations for certain classes of analytic vector fields

Keywords

bisimulation equivalence; decidability; finite state machines; reachability analysis; set theory; analytic vector fields; bisimulations; decidability questions; finite state quotients; hybrid systems; infinite state system; linear hybrid automata; model theory; reachability analysis; stratification theory; subanalytic sets; timed automata; Automata; Automatic control; Continuous time systems; Design methodology; Differential equations; Formal verification; Logic; Reachability analysis; State-space methods; Vectors;

fLanguage

English

Publisher

ieee

Conference_Titel

Decision and Control, 1998. Proceedings of the 37th IEEE Conference on

Conference_Location

Tampa, FL

ISSN

0191-2216

Print_ISBN

0-7803-4394-8

Type

conf

DOI

10.1109/CDC.1998.758525

Filename

758525