The hybrid phenomena captured by such mathematical models are manifested in a great diversity of complex engineering applications such as real-time systems, embedded software, robotics, mechatronics, aeronautics, and process control. The high-profile and safety-critical nature of such applications has fostered a large and growing body of work on formal methods for hybrid systems: mathematical logic, computational models and methods and automated reasoning tools supporting the formal specification and verification of performance requirements for hybrid systems, and the design and synthesis of control programs for hybrid systems that are provably correct with respect to formal specifications.
This course investigates modeling, analysis and synthesis of various classes of hybrid systems. An introduction to computational and simulation tools for hybrid systems will be given. The course consists of lectures, a handful of homeworks, and a final project.
| Date | Lecturer | Contents |
| January 22 | T. John Koo and S. Shankar Sastry | Introduction |
| January 24 | T. John Koo | Background: Discrete systems |
| January 29 | T. John Koo | Background: Discrete systems |
| January 31 | T. John Koo | Background: Discrete systems |
| February 5 | T. John Koo | Background: Continuous systems |
| February 7 | T. John Koo | Modeling: Hybrid systems |
| February 12 | T. John Koo | Modeling: Hybrid systems |
| February 14 | T. John Koo | Modeling: Hybrid systems |
| February 19 | T. John Koo | Modeling: Hybrid systems |
| February 21 | Tunc Simsek | Simulation: SHIFT |
| February 26 | Jie Liu | Simulation: Ptolemy II |
| February 28 | T. John Koo | Project Overview |
| March 5 | T. John Koo | Analysis: Stability of hybrid systems |
| March 7 | T. John Koo | Analysis: Stability of hybrid systems |
| March 12 | T. John Koo | Analysis: Reachability |
| March 14 | T. John Koo | Analysis: Bisimulation |
| March 19 | T. John Koo | Analysis: Time Automata |
| March 21 | T. John Koo | Analysis: Time Automata |
| March 26 | T. John Koo | No Class |
| March 28 | T. John Koo | No Class |
| April 2 | Howard Wong-Toi | Analysis: Linear hybrid automata |
| April 4 | Howard Wong-Toi | Computation: HYTECH |
| April 9 | T. John Koo | Synthesis: Multi-modal control |
| April 11 | T. John Koo | Synthesis: Multi-modal control |
| April 16 | S. Shankar Sastry | Synthesis: Optimal Control |
| April 18 | S. Shankar Sastry | Synthesis: Game Theory |
| April 23 | T. John Koo | Synthesis: Controller synthesis |
| April 25 | T. John Koo | Synthesis: Controller synthesis |
| April 30 | Jianghai Hu | Advanced Topics: Stochastic hybrid systems |
| May 2 | Slobodan Simic | Advanced Topics: Geometric theory of hybrid systems |
| May 7 | T. John Koo | Advanced Topics: Embedded control systems |
| 9:20 | Darren Liccardo | Control Mode Switching, A Design Example for Ship-Deck Landing |
| 9:40 | Weehong Tan | Gain Scheduling and Hybrid Systems |
| 10:00 | Shannon Zelinski | A Hybrid Solution To Changing Formation For Autonomous Formation Flight |
| 10:20 | Gabriel Eirea and Matt Senesky | Hybrid Control of a Two Output DC-DC Converter |
| 10:40 | Aaron Ames | Functional Representation of If Statements |
| 11:00 | Sinem Coleri and Mustafa Ergen | Verification and Power Analysis of an Event-Based System, TinyOS, with Hybrid Automata for Sensor Networks |
| 11:20 | Mark Wilcutts | Hybrid System Verification using CheckMate |
| 11:40 | Srinath Avadhanula | Reachability Analysis of 2 DOF LTI Systems |
| 12:00 | Guang Lu | Autonomous Vehicle Following Lateral Control Using Hybrid Automata |
| 12:20 | Kunpeng Sun | Extensions of Jump Markov System Estimation Techniques |
| 12:40 | Rodney A. Martin | Synthesis of an Optimal Reference Signal Modification Strategy in Response to Thermal Sensation Complaints for Building Operations |
| 1:00 | Arkadeb Ghosal | A Methodology for the Implementation and Verification of Hybrid Systems |
| 1:20 | Songhwai Oh | Learning to Fly: a Mission-Oriented Flight Control with Collision Avoidance |
| 1:40 | Joseph E. Barton | Modeling an Internal Combustion Engine Under Sliding Mode Control as a Hybrid System |
Gain Scheduling and Hybrid Systems
Weehong Tan
Gain scheduling is a control method that is widely used in the industry
because it is both an effective and economical method for nonlinear control.
Despite its widespread use in practice, there is very little theoretical
research on gain scheduling until the last decade. Traditionally,
most gain scheduling methods still rely on extensive simulation for the
evaluation of stability and performance for the overall system. This paper
is an attempt to find a systematic approach to analyzing the overall gain
scheduling stability and performance by using the framework in control
mode switching and the hybrid systems tools, thereby eliminating the need
for extensive simulation.
A Hybrid Solution To Changing Formation For Autonomous Formation
Flight
Shannon Zelinski
This project explores a hybrid solution to changing formation for the
formation flight of unmanned aerial vehicles (UAVs). The principals of
hybrid systems are used to separate the continuous control of formation
flying UAVs from the discrete logic of changing formation. The ideas of
the leader relative axis, formation change libraries, and leader-follower
switching are presented as well as an algorithm for finding feasible continuous
trajectories for a formation change. The algorithm can be used off line
to create the formation change libraries. A formation of UAVs can use relatively
few libraries along with leader-follower mode switching to find a reachable
sequence for a multitude of different formation changes.
Hybrid Control of a Two Output DC-DC Converter
Gabriel Eirea and Matt Senesky
Switched circuits in power electronics by their nature present hybrid
behavior. Control is accomplished by switching between discrete states
with linear dynamics. We describe the characteristics of a two output
DC-DC converter using only one inductor. Several approaches for the
calculation of the safe set of operating points are presented along with
stability analysis. Controller synthesis is discussed, and several ad hoc
control methods and corresponding results are described.
Functional Representation of If Statements
Aaron Ames
Given a sequence of $k$ functions, $(f_n(x))_{n=1}^{k}$ for $x \in
\mathbb{R}^n$, and $n-1$ conditional statements relating the functions,
I will find a single function that converges uniformly to $(f_n(x))_{n=1}^{k}$
for all $n$. The flow generation of any number of discontinuous differential
equations related by switching conditions will be considered as a specific
application.
Verification and Power Analysis of an Event-Based System, TinyOS,
with Hybrid Automata for Sensor Networks
Sinem Coleri and Mustafa Ergen
The advances in digital circuitry and sensor technology has enabled
reliable monitoring of environments through wireless microsensor systems.
Event driven operating system has been shown to meet the requirements of
such platforms. In this paper, we focus on TinyOS, an event-based operating
system for Smart Dust networked sensors. We show how to model TinyOS as
a hybrid automata by using the tool HYTECH and verify the correct operation
of the system by using safety verification feature of HYTECH. Since lifetime
is a important metric for sensor nodes that are planned to be deployed
once and unattended for long periods of time without maintenance, we perform
power analysis of a sensor node by using trace generation feature of HYTECH.
Furthermore, we simulate a tree sensor network of TinyOS motes by using
the programming language SHIFT to determine the lifetime of the network
as a function of the distance from the central data collector.
Hybrid System Verification using CheckMate
Mark Wilcutts
CheckMate is a computational tool for formally verifying hybrid dynamic
systems, developed at Carnegie Mellon University. This talk will focus
on what class of systems the tool can help with, and sketch how the tool
works. Some simple examples will illustrate fundamental concepts, and an
example from automotive control systems will show how the tool can be used
in a practical situation.
Reachability Analysis of 2 DOF LTI Systems
Srinath Avadhanula
We present reachability analysis of 2 DOF linear time invariant systems.
This work builds upon previous work by Krogh et al. It utilizes the various
properties of LTI systems to come up with a method which minimizes the
computation required to generate a reach set. This analysis is then used
for verification and validation. We present implementation of this algorithm
to various test cases to demonstrate the features of the method.
Autonomous Vehicle Following Lateral Control Using Hybrid Automata
Guang Lu
Autonomous vehicle following control is a control scheme in which the
controlled vehicle follows the trajectory of its preceding vehicle.
The goal of vehicle lateral control is lane-keeping. However, the
performance of the following vehicle depends on the performance of its
preceding vehicle, i.e. the lateral deviation of the preceding vehicle
will result in worse performance of the vehicle that follows it.
In this project, I will show how this vehicle following algorithm can be
improved by using hybrid automata.
Extensions of Jump Markov System Estimation Techniques
Kunpeng Sun
In this note, some estimation techniques in jump Markov systems are
reviewed, then a special case of an estimation problem is considered, where
the Viterbi algorithm holds, allowing the maximum a posterior model sequence
to be computed recursively in time. In the same case, another algorithm
is derived to compute the exact posterior model probabilities at each time
step, with fixed computation in each time step. Furthermore, a new heuristic
algorithm is proposed to calculate the posterior model probabilities for
the general model. An example is used to illustrate the performance of
the algorithm.
Synthesis of an Optimal Reference Signal Modification Strategy
in Response to Thermal Sensation Complaints for Building Operations
Rodney A. Martin
The objective of this study is to compare an optimal reference modification
strategy for a closed-loop system developed by Hansson [8] with other ad-hoc
and Monte Carlo techniques. Hansson's method uses information about critical
discrete events that occur during system operation in a theoretically optimal
fashion. The discrete events are associated with upcrossings of a stationary
process above some critical level. It is assumed that a controller is already
designed for the system, and corrective actions are performed only with
modification of the reference signal. Therefore the strategy is suitable
for use in operating plants without having to take the system offline for
tuning of the existing controller. The solution will be tested for an HVAC
thermal comfort application where there are two levels: for hot complaints
and cold complaints, rather than just one level. It has been found that
the design may need to include allowances for obtaining information from
both levels at the instance of any particular event, rather than just one
level.
A Methodology for the Implementation and Verification of Hybrid
Systems
Arkadeb Ghosal
The aim of the project is to propose a methodology to design, implement
and analyze hybrid dynamical systems. This is based around two concepts
-- Masaccio, a formal modelling language, and Giotto, a time-triggered
programming language. Masaccio is used to model the specification of a
system and Giotto is used to implement the software part. The two verification
tasks which are required to be carried out are: verification of safety
and analysis of the refinement done while modelling. This report gives
a broad view of the project, formalizes Giotto-Masaccio translation and
proposes a relaxed notion of refinement. Refinement is prametereized by
allowing discrepancies between implementation and specification in values
and time of the system.
Learning to Fly: a Mission-Oriented Flight Control with Collision
Avoidance
Songhwai Oh
The problem of designing a flight controller which can steer a plane
to the destination with minimal cost while avoiding collisions with obstacles
is considered. The controller does not have a prior knowledge about the
locations of the obstacles and this is different from the previous approaches.
First, the complexity of the problem is reduced by considering only a finite
set of controls. Next, the problem is formulated as a Markov decision problem.
Finally, the reinforcement learning is used to find a reactive controller
that is computationally efficient and optimal within the policy class.
Modeling an Internal Combustion Engine Under Sliding Mode Control
as a Hybrid System
Joseph E. Barton
This project models an internal combustion engine under sliding mode
control. The controller has the combined task of achieving desired
vehicle speeds while limiting emissions and vehicle acceleration for passenger
comfort. The major components of the engine are modelled as individual
modules, allowing more sophisticate sub-models to be incorporated at a
later time.