Modeling and verification of hybrid systems with clocked and unclocked events

We define sampled-data hybrid automata (SDHA), to model systems with clocked and unclocked events. Although clocked events can be modeled in standard hybrid automata by introducing additional continuous state variables, we show in this paper how the SDHA formalism provides a basis for more efficient...

Full description

Saved in:
Bibliographic Details
Main Authors: Silva, B.I., Krogh, B.H.
Format: Conference Proceeding
Language:English
Subjects:
Automata
Automatic control
Clocks
Control systems
Frequency
Jitter
Logic
Microwave integrated circuits
Sampling methods
Uncertainty
Online Access:Request full text
Tags: Add Tag
No Tags, Be the first to tag this record!
Description
Summary:We define sampled-data hybrid automata (SDHA), to model systems with clocked and unclocked events. Although clocked events can be modeled in standard hybrid automata by introducing additional continuous state variables, we show in this paper how the SDHA formalism provides a basis for more efficient computational methods for verification. Towards this end, we define a transition system semantics for the SDHA and present a method for computing approximate quotient transition systems using a modification of existing tools for computing reachable sets for hybrid systems. The definitions and the elements of a model checking procedure for SDHA are illustrated with an example.
DOI:10.1109/CDC.2001.980198