This tutorial gives an introduction to hybrid systems, which are systems where continuous dynamics (usually defined in terms of differential equations) interact with discrete aspects (often modelled in terms of automata). First an intuitive background is given on key concepts from dynamical systems, and systems and control theory. Then an overview is given of several research topics within hybrid systems.
The main focus is not on in-depth technical treatment, but on giving a computer science audience a conceptual flavour of some of the major topics in this challenging multi-disciplinary field. The tutorial consists of three parts:
An introduction is given to input-state-output systems. It is shown how to obtain explicit representations of the behaviour for linear time invariant systems. Non-linear systems can locally be linearized. The properties of controllability and observabilty are introduced, together with criteria for checking these properties.
Several research issues are presented, like Zeno behaviour and decidability (together with restricted classes of hybrid systems). An overview is given on hybrid systems tools. The basic idea behind controller synthesis is sketched. Some fundamental concepts in optimal control are presented.
This talk presents the first results of an OOTI-project, called COMM, carried out in the context of the Boderc project. The research topic of Boderc is multi-disciplinary system-controller design. The carrying industrial partner of this project is Océ. The main approach in Boderc is to couple models of different disciplines. Within the COMM project we investigate the simulation of real-time embedded systems, where software and physical components interact with each other. This requires coupling of modeling tools from different disciplines. Since at Océ Rose-RT and Matlab/Simulink are used, we selected these tools for coupling. The goal of this presentation is to show the possibilities and problems of coupling of Rose-RT and Matlab/Simulink.
We discuss a process algebra that is intended as an algebraic framework for the description and analysis of hybrid systems. It comprises: mathematical expressions for hybrid systems, equational axioms for equational reasoning about hybrid systems, rules for lifting results from real analysis to equations about hybrid systems, and a structural operational semantics of the expressions. The process algebra is obtained by extending a combination of two existing process algebras, namely the process algebra with continuous relative timing of Baeten and Middelburg (2001) and the process algebra with propositional signals of Baeten and Bergstra (1997). The choice of the operators that have been added to the combination has been strongly influenced by the formalism of hybrid automata. The discussion of this process algebra for hybrid systems will concentrate on the following points: main design choices, main features, relevance to the field of hybrid systems, and relationship to hybrid automata and the above-mentioned process algebra with timing.
Note: The process algebra for hybrid systems is the result of joint work with Jan Bergstra from the University of Amsterdam and Utrecht University.
Action safety of a hybrid process, is the property that a certain undesired action never takes place during any of the possible executions of that process. Similarly, predicate safety, means that a certain predicate on the variables that play a role in the process, never evaluates to true. In this presentation, we study these two types of safety properties, by giving a process algebraic specification for them, in the hybrid process algebra HyPA. Then, we show through algebraic reasoning, a general method to reduce the question of safety of a linear process definition, to the question of safety of its subprocesses. As an example, we apply this method to a variant of Fischer's protocol for mutual exclusion. This variant makes use of the assumption that there is a maximum relative error between the clocks in the protocol, which calls for a certain interaction between continuously changing variables. This makes the example hybrid in nature, and clearly displays some of the specific problems that arise when verifying safety of hybrid systems in general.
In the behavioural approach to control engineering continuous dynamical systems are not characterized by relating a priori chosen input and output variables, but by defining sets of admissable time-trajectories that map signals to values in a suitable signal space. This leads to a more general way of modelling that does not unnecessarily constrain the interpretation of signals as inputs or outputs. In electrical circuits, for instance, there is often a choice between selecting voltage as input and current as output, or vice versa.
The behavioural approach also supports a notion of system composition (or interconnection) via intersection of the admissable trajectory sets of common signals. This composition mechanism, as well as the abstraction from committed input/output signals are well-aligned with the principles of classical process calculi with concurrent composition and action synchronization.
In our talk we will present a process calculus for the description and analysis of hybrid systems in a behavioural setting. To describe continuous behaviour the usual set of operators for the description of discrete behaviour is extended with a trajectory-prefix operator, and the classical choice or summation is replaced by a powerful superposition operator that suitably merges sets of trajectory-prefixes.
We will show how this calculus elegantly links the modelling of discrete, real-time, hybrid, and continuous systems. It has classical calculi for discrete and real-time behaviour as sub-calculi, and also provides a compositional formalism for the description purely continuous dynamical systems. We will discuss how hybrid automata can be represented in the calculus and present worked examples of a few hybrid and continuous systems.
First a notion of bisimulation is developed for continuous systems as ordinarily studied in systems and control theory. An algebraic characterization of bisimulation together with an algorithm for computing the maximal bisimulation relation is derived using geometric control theory. Bisimulation of continuous systems is shown to be a concept which unifies the system-theoretic concepts of state space equivalence and state space reduction, and which allows to study equivalence of systems with non-minimal state space dimension. Secondly, by merging bisimulation of continuous systems with bisimulation of labeled transition systems a notion of structural bisimulation is introduced for hybrid systems with continuous input and output variables.
Consider a dynamical system described by a system of differential equations of the form
with the property that
. If the system would be initialized in
then, at least theoretically, the system would
remain in equilibrium for all time. Consider for instance a
rigid rod balancing upright on a flat surface. If the rod is
perfectly vertical and completely at rest then it should
remain in that position. However, in practice it is of
course not possible to realize this. The slightest
deviation of the upright position will cause the rod to
fall. We call the upright position an unstable
equilibrium. On the other hand a rod hanging downwards
from, eg., your hand has a stable equilibrium.
Loosely speaking, a stable equilibrium point has the
property that 
stays close to the equilibrium
provided that it is initialized sufficiently close to that
equilibrium.
In this presentation we study stability of switched linear systems. These are systems described by linear differential equations of the form
is a finite index set,
, and the 
s are 
real
matrices. At certain instants of time, called switching
times, the system dynamics, i.e. the matrix switches
from one matrix to the other. A switch could be caused by,
e.g.,
deliberate action from outside, it could be caused by an
event in the state space, or for some other reason.
The problem
that we want to study is under which conditions is the zero
solution a stable equilibrium point. A special case of this
problem is the case where there is no switching at all. In
that case the dynamics is given by
Already in the case that the system dynamics changes between
two modes, 
and 
, the situation is considerably
more complicated.
The presentation contains the following subjects:
Piecewise Deterministic Markov Processes (PDPs) form a class of stochastic hybrid processes covering almost all applications that do not contain diffusion. A PDP is a mixture of deterministic continuous motion and of random jumps and therefore exhibits a hybrid behavior. In this talk we focus on communicating PDPs (CPDPs) which are specified within an automaton-framework that is used for compositional specification of PDP systems. We introduce a parallel composition operator for CPDPs and show how CPDP-subsystems can be composed to form one PDP (which is of distributed nature). We show that there is a close relation between PDPs and CPDPs in the sense that they bring forth the same stochastic processes. Therefore, known stochastic analysis techniques for PDPs can also be applied to composite CPDPs.
Timed I/O Automata (TIOA) has been recently introduced modeling framework for timed systems. It is evolved as a special class of Hybrid I/O Automata (HIOA) of Lynch, Segala and Vaandrager by excluding external variables that model continuous information flow. In a TIOA the state of the automaton may change in two ways: by discrete transitions, which change the state atomically, and by trajectories. Trajectories describe the evolution of a state over intervals of time. Trajectories are specified by: "satisfies predicates" which must be satisfied by all trajectories, and "stops-when predicates" which state the upper bound of the trajectory. Following early works of Bornot and Sifakis 1998 on deadline predicates, we propose the use of urgency predicates instead of stops-when predicates for specifying upper bound on timing delays. The urgency predicate is introduced in every transition definition, and the upper bound of the trajectory is the time when the precondition and urgency predicate of the transition become true. The advantage of using urgency predicate over stop-when predicate is: (1)It leads to shorter and more natural specifications. (2) Under some reasonable assumptions, it ensures time reactivity, (i.e., whenever time progress stops there exists at least one enabled transition). In this talk, I will introduce urgency predicates, illustrate their use with some examples, and present results related to expressively, compositionality and verification.
We present a framework for working with automata (in general) in PVS; this framework is very flexible, which allows for automaton specifications with varying levels of structure and, of course, hybrid elements as well. Some basics of working in PVS will be presented, followed by the automaton framework and a method for specifying hybrid behavior. An example, based on the BART train system control, is presented, and we pause a moment to examine the trouble that using complex arithmetic expressions (for the differnetial equations) gives us in PVS. Some suggestions for improvement and future work will be given as well.
To spur the interest of the program verification research community to consider the formal specification and mechanical verification of programs that interact with their environment, Earl Boebert proposed - in 1982 - to consider the simple task of steering a vehicle down a straighline course in a crosswind that varies with time. The challenge he formulated was to state formally what it means to keep the vehicle on course, and, for some particular control problem, prove mechanically that the program satisfies its high level specification. A first solution to this problem was proposed by R.S. Boyer, M.W. Green and J.S. Moore in 1982, i.e., almost a decade before hybrid systems became a fashionable as a research topic.
In this paper, we reconsider Boebert's challenge and present two solutions using modern insights from hybrid systems research and the verification tools Uppaal and PVS.
HybridUML is an extension of UML for the purpose of modeling hybrid systems. The construction uses the profile mechanism of UML 2.0 which is the standard procedure for extending the Unified Modeling Language. The "intuitive semantics" of the syntactic extension is based on straightforward semantics for hierarchical Hybrid Automata. However, our approach associates formal semantics by definition of a transformation for Hybrid UML constructs into an executable "low-level" language which is both executable in hard real-time and semantically well-defined. When compared to approaches assigning semantics directly to the high-level constructs of a formal specification language, the transformation approach offers two main advantages: First, the semantics can be more easily adapted to syntactic extensions by extending the transformation in an appropriate way. Second, HybridUML specifications can be compiled into executable code which is suitable for execution in hard real-time on multi-processor computers. This serves both for the development of systems and for specification-based testing in real-time.
Apart from describing the specification capabilities offered by the new profile, we illustrate the transformation concept and the semantic model of the executable target language. Other areas of interest - such as hard real-time simulation and automated test data generation against HybridUML specifications - will be briefly discussed. The concepts as well as the "look-and-feel" of the new UML profile are illustrated by facets of a larger case study.
An overview is given of the hybrid Chi formalism and associated tools. Chi is compared to other hybrid formalisms and design considerations are presented. The hybrid Chi formalism integrates concepts from the dynamics and control theory with concepts from computer science. It also integrates a high expressivity with an elegant straightforward semantics. Where modeling and simulation languages cannot be used for verification, and verification formalism are often cumbersome for modeling, Chi is suited to both. The application domain of Chi, which ranges from complete factories to machine control and physical phenomena, is treated and some examples are given.
The syntax and structured operational semantics of hybrid Chi are discussed. The Chi language has a relatively large number of operators for discrete-event modeling, but it also allows specification of general differential algebraic equations, such as higher index systems. Its process instantiation mechanism enables encapsulation, hierarchical composition and reuse of processes. Modular composition is supported by means of parallel composition, and by means of different interaction mechanisms: handshake synchronization and synchronous communication for discrete-event processes, and shared variables for continuous-time processes. Examples are given to illustrate the language.
A hybrid automaton is one of the most popular formal models for hybrid system specification. A formal translation is defined from hybrid automata to Chi and vice versa. The goal of the formal translation from a Chi model to a hybrid automaton is to enable verification of properties of hybrid Chi models using existing model checkers for hybrid automata, such as HyTech. Examples are given to illustrate the use of the translations.