An Introduction to Hybrid Automata, Numerical Simulation and Reachability Analysis
Hybrid automata combine finite state models with continuous variables that are governed by differential equations. Hybrid automata are used to model systems in a wide range of domains such as automotive control, robotics, electronic circuits, systems biol
- PDF / 700,458 Bytes
- 32 Pages / 476.221 x 680.315 pts Page_size
- 57 Downloads / 217 Views
Abstract. Hybrid automata combine finite state models with continuous variables that are governed by differential equations. Hybrid automata are used to model systems in a wide range of domains such as automotive control, robotics, electronic circuits, systems biology, and health care. Numerical simulation approximates the evolution of the variables with a sequence of points in discretized time. This highly scalable technique is widely used in engineering and design, but it is difficult to simulate all representative behaviors of a system. To ensure that no critical behaviors are missed, reachability analysis aims at accurately and quickly computing a cover of the states of the system that are reachable from a given set of initial states. Reachability can be used to formally show safety and bounded liveness properties. This chapter outlines the major concepts and discusses advantages and shortcomings of the different techniques.
1
Introduction
Hybrid automata are a modeling formalism that combines discrete states with continuously evolving, real-valued variables. The discrete states and the possible transitions from one state to another are described with a finite state-transition system. A change in discrete state can update the continuous variables and modify the set of differential equations that describes how variables evolve with time. Hybrid automata are non-deterministic, which means that different futures may be available from any given state. Rates of change or variable updates can be described by providing bounds instead of fixed numbers. Incomplete knowledge about initial conditions, perturbations, parameters, etc. can easily be captured this way. Hybrid automata capture a rich variety of behaviors, and are used in a wide range of domains such as automotive control, robotics, electronic circuits, systems biology, and health care. The hybrid automaton model is well-suited for formal analysis, in the sense that sets of behaviors are readily described by mathematical equations. In the next section, we present the hybrid automaton formalism with an example and give a formal definition of the model and its semantics. Behaviors of hybrid automata are computed in practice using numerical simulation, which
R. Drechsler, U. Kühne (eds.), Formal Modeling and Verification of Cyber-Physical Systems, DOI 10.1007/978-3-658-09994-7_3, © Springer Fachmedien Wiesbaden 2015
An Introduction to Hybrid Automata xr + L
xr + L
xr
x xr
51
m
Fs
Fg
m Fg
x
(a) extension
(b) freefall
Fig. 1. A ball suspended from a ceiling by an elastic string
is presented in Sect. 3. We discuss major aspects such as approximation errors, stability, stiffness and Zeno behavior. Simulation techniques have recently been extended to provide formal guarantees for certain classes of systems. Reachability techniques are discussed in Sect. 4. Different algorithms and data structures are suitable for reachability, depending mainly on the type of dynamics: piecewise constant, affine, and nonlinear. We present an overview of the main techniques, with part
Data Loading...
